blob: 5d9049304d7ee7f33edbe884315674a177c9ba9c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(*
Example proof script for Isabelle Proof General.
$Id$
Same as Example.ML, except using X-Symbol input tokens.
*)
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";
|