diff options
| -rw-r--r-- | isar/Example.thy | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index f6500e6d..7b4fdcac 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -8,17 +8,16 @@ you may get the theory mode of ordinary Isabelle Proof General *) +theory Example = Main: -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; +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" + thus "B & A" + proof + assume A B + show ?thesis + .. + qed +qed +end |