aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--etc/release-log.txt4
-rw-r--r--isa/isa.el5
2 files changed, 6 insertions, 3 deletions
diff --git a/etc/release-log.txt b/etc/release-log.txt
index 66d5d2f6..ce5d4c2b 100644
--- a/etc/release-log.txt
+++ b/etc/release-log.txt
@@ -1,3 +1,7 @@
+9.05.00 3.1.5 Release 3-1-5, from Release-3-1-branch
+ Improved proof-find-theorems-command for Isabelle
+ (allow multiple constants separated by commas).
+
28.04.00 3.1.4 Release 3-1-4, from Release-3-1-branch
Applied patch sent by Mike Squire, fix accident in previous fix.
(Isabelle theory retraction file paths)
diff --git a/isa/isa.el b/isa/isa.el
index 0f4a69dd..d6adba79 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -76,8 +76,7 @@ no regular or easily discernable structure."
(list isa-docs-menu))
"Entries for Isabelle menu.")
-(proof-deftoggle isabelle-show-sorts)
-(proof-deftoggle isabelle-show-types)
+
;;;
@@ -141,7 +140,7 @@ and script mode."
proof-context-command "ProofGeneral.show_context()"
proof-info-command "ProofGeneral.help()"
proof-kill-goal-command "ProofGeneral.kill_goal();"
- proof-find-theorems-command "ProofGeneral.thms_containing [\"%s\"]"
+ proof-find-theorems-command "ProofGeneral.thms_containing (space_explode \",\" \"%s\");"
proof-shell-start-silent-cmd "proofgeneral_disable_pr();"
proof-shell-stop-silent-cmd "proofgeneral_enable_pr();"
;; command hooks