From 304cf41b762c57bda2f1176fc8c366e9801015d2 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 3 Dec 2009 00:26:21 +0000
Subject: Change of type for proof-script-span-context-menu-extensions

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

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

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
index 6d2f69ec..8856eba4 100644
--- a/isar/Example-Tokens.thy
+++ b/isar/Example-Tokens.thy
@@ -13,21 +13,12 @@ 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