From 876bf804fcd7ed07c6b6cd8af5f5ac0bf348eea1 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Tue, 4 Sep 2001 19:19:57 +0000
Subject: tuned proof text; added script version;

---
 isar/Example.thy | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 22c0a4e1..179b5b83 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -11,15 +11,27 @@
 
 theory Example = Main:
 
+text {* Proper proof text. *}
+
 theorem and_comms: "A & B --> B & A"
 proof
   assume "A & B"
   thus "B & A"
   proof
-    assume A B
-    show ?thesis 
-      ..
+    assume B and A
+    thus ?thesis ..
   qed
 qed
 
+
+text {* Proof script. *}
+
+theorem "A & B --> B & A"
+  apply (rule impI)
+  apply (erule conjE)
+  apply (rule conjI)
+   apply assumption
+  apply assumption
+  done
+
 end
-- 
cgit v1.2.3