blob: a8922e87b62c5588c1a6336d18531c94f9bcd0f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(*
Example proof script for Isabelle
David Aspinall <da@dcs.ed.ac.uk>
$Id$
*)
goal HOL.thy
"(A & B)-->(B & A)";
br impI 1;
br conjI 1;
be conjE 1;
ba 1;
be conjE 1;
ba 1;
qed "and_comms";
|