blob: 24a33651cd836d1acf3a6aec367d17352f7d3f95 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Test printing of Tactic Notation *)
Tactic Notation "a" constr(x) := apply x.
Tactic Notation "e" constr(x) := exact x.
Lemma test : True -> True /\ True.
intro H; split; [a H|e H].
Show Script.
Qed.
|