From c440ded61788d0718065c494f7f19065da0e7e03 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 20 Aug 2009 11:00:44 +0000
Subject: Remove spurious junk.

---
 isar/Example.thy | 31 +------------------------------
 1 file changed, 1 insertion(+), 30 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 16114823..34c840fe 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -18,38 +18,9 @@ proof
  qed
 qed
 
-(* 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
-  assume "A & B"
-  then obtain B and A ..
-  then show "B & A" .. 
-qed
-
-
 text {* Unstructured proof script. *}
 
-theorem  "A & B --> B & A" -- {* foo bar *}
+theorem  "A & B --> B & A"
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
-- 
cgit v1.2.3

