From bfd4724e70dd6e03fe8f391b7736ce67b15b3616 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 1 Jun 2000 13:41:31 +0000
Subject: Removed now spurious semicolons, 8-).

---
 isar/Example.thy | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'isar/Example.thy')

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
-- 
cgit v1.2.3