diff options
-rw-r--r-- | isar/Example.thy | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 7b4fdcac..6abc15e1 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -1,11 +1,11 @@ (* -*- isar -*- - Example proof document for Isabelle/Isar Proof General. - - $Id$ + 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 + The first line forces Isabelle/Isar Proof General, otherwise + you may get the theory mode of ordinary Isabelle Proof General *) theory Example = Main: @@ -13,11 +13,12 @@ theory Example = Main: theorem and_comms: "A & B --> B & A" proof assume "A & B" - thus "B & A" - proof - assume A B - show ?thesis - .. - qed + thus "B & A" + proof + assume A B + show ?thesis + .. + qed qed + end |