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 +----------
 isar/Example.thy        |  2 ++
 isar/isabelle-system.el |  2 +-
 3 files changed, 4 insertions(+), 11 deletions(-)

(limited to 'isar')

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
diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..a826cae8 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -19,6 +19,8 @@ proof
  qed
 qed
 
+(* quite nice I think but what if I type here? *)
+
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index f66e41ba..ec405b13 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -342,7 +342,7 @@ for you, you should disable this behaviour."
 ;;
 
 (defun isabelle-create-span-menu (span idiom name)
-  (if (string-equal idiom "proof")
+  (if (eq idiom 'proof)
       (let ((thm (span-property span 'name)))
 	(list (vector
 	       "Visualise dependencies"
-- 
cgit v1.2.3