diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-10-27 13:01:36 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-10-27 13:01:36 +0000 |
| commit | fed6e45d564a7e2793540e1906e37fe8a8b2ea87 (patch) | |
| tree | 43b141e3c5c49d95d8c993d65aa673a268f4c6eb /generic/proof-script.el | |
| parent | 77b4bf5412d1ea96d3b70b12db3549b2fa4727b1 (diff) | |
tuned msg;
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 5b7492a0..5b4a5123 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -448,7 +448,7 @@ proof assistant and Emacs is has a modified buffer visiting the file." (buffer (proof-file-to-buffer cfile))) (proof-debug (concat "Registering file " cfile (if (member cfile proof-included-files-list) - " (already registered, no action)." "."))) + " (already registered, no action)" ""))) (unless (member cfile proof-included-files-list) (and buffer (not informprover) @@ -543,7 +543,7 @@ retracted using proof-auto-retract-dependencies." (concat "Unregistering file " cfile (if (not (member cfile proof-included-files-list)) - " (not registered, no action)." "."))) + " (not registered, no action)" ""))) (if (member cfile proof-included-files-list) (progn (proof-auto-retract-dependencies cfile informprover) @@ -1897,9 +1897,9 @@ This is intended as a value for proof-activate-scripting-hook" ;; (proof-define-assistant-command-witharg proof-find-theorems - "Search for items containing a given constant." + "Search for items containing given constants." proof-find-theorems-command - "Find theorems containing the constant" + "Find theorems containing the constant(s)" (proof-shell-invisible-command arg)) (proof-define-assistant-command-witharg proof-issue-goal |