From d3b4b2055a531970d4f9cef917c9aac86fd7d35f Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 3 Dec 2009 00:28:09 +0000
Subject: Revert spurious commits

---
 isar/Example-Tokens.thy | 11 ++++++++++-
 isar/Example.thy        |  2 --
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'isar')

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
index 8856eba4..6d2f69ec 100644
--- a/isar/Example-Tokens.thy
+++ b/isar/Example-Tokens.thy
@@ -13,12 +13,21 @@ theory "Example-Xsym" imports Main begin
 
 text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *}
 
+theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>"
+proof
+  assume "\<phi> \<and> \<psi>"
+  then show "\<psi> \<and> \<phi>"
+  proof
+    assume \<psi> and \<phi>
+    then show ?thesis ..
+ qed
+qed
+
 text {* \<^bbold>Unstructured\<^ebold> proof script. *}
 
 theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> \<phi>\<^isub>\<beta> \<and> \<phi>\<^isub>\<alpha>"
   apply (rule impI)
   apply (erule conjE)
-  
   apply (rule conjI)
   apply assumption
   apply assumption
diff --git a/isar/Example.thy b/isar/Example.thy
index a826cae8..720e5480 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -19,8 +19,6 @@ proof
  qed
 qed
 
-(* quite nice I think but what if I type here? *)
-
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
-- 
cgit v1.2.3