From 102c8aea283a732e17dfd557f2b93cec045ec413 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Thu, 27 Dec 2001 15:56:52 +0000
Subject: tuned;

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

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 179b5b83..357fa09e 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -11,20 +11,30 @@
 
 theory Example = Main:
 
-text {* Proper proof text. *}
+text {* Proper proof text -- naive version. *}
 
 theorem and_comms: "A & B --> B & A"
 proof
   assume "A & B"
-  thus "B & A"
+  then show "B & A"
   proof
     assume B and A
-    thus ?thesis ..
+    then show ?thesis ..
   qed
 qed
 
 
-text {* Proof script. *}
+text {* Proper proof text -- advanced version. *}
+
+theorem "A & B --> B & A"
+proof
+  assume "A & B"
+  then obtain B and A ..
+  then show "B & A" ..
+qed
+
+
+text {* Unstructured proof script. *}
 
 theorem "A & B --> B & A"
   apply (rule impI)
-- 
cgit v1.2.3