isa/example.ML


1
2
3
4
5
6
7
8
9
10
11
12
13
14

(*
    Example proof script for Isabelle Proof General.

    $Id$
*)    

Goal "(A & B)-->(B & A)";
br impI 1;
br conjI 1;
be conjE 1;
ba 1;
be conjE 1;
ba 1;
qed "and_comms";