blob: 805e69fb9f35107cdbe90bebb9ddf54808e90c62 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Any (* nested comments *) are tricky in XEmacs (21.4.8),
but better syntax handling in Emacs at the moment.
*)
Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
by (rtac impI 1);
by (etac conjE 1);
by (rtac conjI 1);
by (assume_tac 1);
by (assume_tac 1);
qed "and_comms";
(* Comment at the end?! *)
|
