From c8cd8ace98d6e0f3ebdce7718d92229f0c31dbec Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 17 Aug 2009 16:45:41 +0000
Subject: Move proof-interrupt-process to proof-shell.  Add pending interrupt
 behaviour.  See http://proofgeneral.inf.ed.ac.uk/trac/ticket/179

---
 isar/Example.thy | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index e869364b..16114823 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -18,7 +18,26 @@ proof
  qed
 qed
 
-text {* Proper proof text -- \textit{advanced version}. *}
+(* but on the other hand, who knows? *)
+
+text {* Proper proof text -- \textit{advanced ve"rs"ion}. What do you think?  Who knows. *}
+theorem "B & A --> A & B"
+proof
+  assume "B & A"  -- "one of those kinds"
+  then obtain A and B ..
+  then show "A & B" ..
+qed 
+
+
+(* foo bar wiggle *)
+
+theorem "A & B --> B & A"
+proof
+  assume "A & B"
+  then obtain B and A ..
+  then show "B & A" .. 
+qed
+
 
 theorem "A & B --> B & A"
 proof
@@ -30,7 +49,7 @@ qed
 
 text {* Unstructured proof script. *}
 
-theorem "A & B --> B & A"
+theorem  "A & B --> B & A" -- {* foo bar *}
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
-- 
cgit v1.2.3