diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:53:12 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:53:12 +0000 |
| commit | 7c9810c7a262715e06a017ad2cedbdf62f4a7a14 (patch) | |
| tree | 12317272c0b4fe8dbbe334b9198f3c89f950b344 | |
| parent | 81956504f52a67275d0f267ab259aaafe6300d8c (diff) | |
proper indentation;
| -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 |