Removed now spurious semicolons, 8-).

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