isar/Example.thy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

(*  -*- isar -*-

    Example proof document for Isabelle/Isar Proof General.
 
    $Id$

    The first line forces Isabelle/Isar Proof General, otherwise
    you may get the theory mode of ordinary Isabelle Proof General
*)


theory Example = Main:;

theorem and_comms: "A & B --> B & A";
proof;
  assume "A & B";
  thus "B & A";
  proof;
    assume A B;
    show ?thesis; ..;
  qed;
qed;

end;