diff options
| -rw-r--r-- | isar/Example.thy | 9 | ||||
| -rw-r--r-- | isar/isar-autotest.el | 3 | ||||
| -rw-r--r-- | isar/isar-find-theorems.el | 32 | ||||
| -rw-r--r-- | isar/isar.el | 19 | ||||
| -rw-r--r-- | lclam/lclam.el | 9 |
5 files changed, 43 insertions, 29 deletions
diff --git a/isar/Example.thy b/isar/Example.thy index 720e5480..b0640146 100644 --- a/isar/Example.thy +++ b/isar/Example.thy @@ -9,10 +9,10 @@ theory Example imports Main begin text {* Proper proof text -- \textit{naive version}. *} -theorem and_comms: "A & B --> B & A" +theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A" proof - assume "A & B" - then show "B & A" + assume "A \<and> B" + then show "B \<and> A" proof assume B and A then show ?thesis .. @@ -22,6 +22,9 @@ qed text {* Unstructured proof script. *} theorem "A & B --> B & A" +by and_comms + + apply (rule impI) apply (erule conjE) apply (rule conjI) diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index cc5d51d7..4ea027be 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -6,6 +6,9 @@ ;; (eval-when-compile + (require 'cl)) + +(eval-when (compile) (require 'proof-utils) (proof-ready-for-assistant 'isar)) diff --git a/isar/isar-find-theorems.el b/isar/isar-find-theorems.el index 0d40f392..15da9f67 100644 --- a/isar/isar-find-theorems.el +++ b/isar/isar-find-theorems.el @@ -10,6 +10,23 @@ ;; $Id$ ;; +(require 'pg-vars) +(declare-function proof-find-theorems "pg-user") + + +;; search form field values + +(defvar isar-find-theorems-data (list + "" ;; num + "" ;; pattern + "none" ;; intro + "none" ;; elim + "none" ;; dest + "" ;; name + "" ;; simp + ) + "Values of the Find Theorems search form's fields.") + ;; make the original (minibuffer based) "Find theorems" command (from ;; ../generic/pg-user.el) available as isar-find-theorems-minibuffer; ;; return '(nil) so that isar-find-theorems-minibuffer works as a @@ -35,7 +52,7 @@ (apply 'isar-find-theorems-create-searchform isar-find-theorems-data) '(nil)) -;; update the universal key bindings (see ../generic/proof-config.el) +;; update the universal key bindings (see ../generic/pg-vars.el) ;; ;; C-c C-a C-m is bound to isar-find-theorems-minibuffer ;; C-c C-a C-f is bound to isar-find-theorems-form @@ -69,19 +86,6 @@ ;; matching the current goal as introduction rule and not having "HOL." ;; in their name (i.e. not being defined in theory HOL). -;; search form field values - -(defvar isar-find-theorems-data (list - "" ;; num - "" ;; pattern - "none" ;; intro - "none" ;; elim - "none" ;; dest - "" ;; name - "" ;; simp - ) - "Values of the Find Theorems search form's fields.") - ;; search form widgets (set in isar-find-theorems-create-searchform ;; and accessed in the "Find" handler) diff --git a/isar/isar.el b/isar/isar.el index 0455ec6d..719d7ce7 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -593,15 +593,16 @@ This slows down interactive processing slightly." (defun isar-preprocessing () "Insert sync markers and other hacks. Uses variables `string' and `scriptspan' passed by dynamic scoping." - (if (proof-string-match isabelle-verbatim-regexp string) - (setq string (match-string 1 string)) - (unless (string-match ";[ \t]*\\'" string) - (setq string (concat string ";"))) - (setq string (concat - "\\<^sync>; " - (isar-shell-adjust-line-width) - string - " \\<^sync>;")))) + (with-no-warnings ; dynamic scoping of string, scriptspan + (if (proof-string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)) + (unless (string-match ";[ \t]*\\'" string) + (setq string (concat string ";"))) + (setq string (concat + "\\<^sync>; " + (isar-shell-adjust-line-width) + string + " \\<^sync>;"))))) ;; ;; Configuring proof output buffer diff --git a/lclam/lclam.el b/lclam/lclam.el index 8bbfb00d..ae83e369 100644 --- a/lclam/lclam.el +++ b/lclam/lclam.el @@ -8,6 +8,9 @@ (require 'proof) ; load generic parts (require 'proof-syntax) +(eval-when-compile + (defvar lclam-toolbar-entries nil)) + ;; ;; =========== User settings for Lambda-CLAM ============ ;; @@ -33,8 +36,8 @@ "Configure Proof General scripting for Lambda-CLAM." (setq proof-terminal-char ?\. - proof-comment-start "/*" - proof-comment-end "*/" + proof-script-comment-start "/*" + proof-script-comment-end "*/" proof-goal-command-regexp "^pds_plan" proof-save-command-regexp nil proof-goal-with-hole-regexp nil @@ -45,7 +48,7 @@ proof-goal-command "^pds_plan %s." proof-save-command nil proof-kill-goal-command nil - proof-assistant-homepage lclam-web-page + proof-assistant-home-page lclam-web-page proof-auto-multiple-files nil proof-prog-name lclam-prog-name proof-shell-process-connection-type t |