From d3b4b2055a531970d4f9cef917c9aac86fd7d35f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 3 Dec 2009 00:28:09 +0000
Subject: Revert spurious commits

---
 isar/Example-Tokens.thy | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'isar/Example-Tokens.thy')

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
-- 
cgit v1.2.3

