diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 09:32:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 09:32:38 +0000 |
| commit | 39697b7a1e8077e8d93a0a0d231388c2ff232a66 (patch) | |
| tree | f547f5f9bdcb6be3e14e4ec332fd8e59866fc544 | |
| parent | d73d4a18026209145b31516b28f4bc863adea051 (diff) | |
Fix to proof-goal-with-hole-result to agree with isar-syntax.el
| -rw-r--r-- | isar/isar.el | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/isar/isar.el b/isar/isar.el index 58e0fa7a..ca77550d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -1,12 +1,15 @@ -;; isar.el Major mode for Isabelle/Isar proof assistant -;; Copyright (C) 1994-2003 LFCS Edinburgh. +;; isar.el Major mode for Isabelle/Isar proof assistant +;; Copyright (C) 1994-2004 LFCS Edinburgh. +;; ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; -;; Maintainer: Stefan Berghofer +;; Maintainers: David Aspinall, Stefan Berghofer ;; ;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Markus Wenzel <wenzelm@in.tum.de> ;; +;; Contributors: David von Oheimb, Sebastian Skalberg +;; ;; ;; $Id$ ;; @@ -139,8 +142,8 @@ See -k option for Isabelle interface script." ;; script buffer. proof-save-command-regexp isar-save-command-regexp proof-goal-command-regexp isar-goal-command-regexp - proof-goal-with-hole-regexp isar-named-entity-regexp ; da - proof-goal-with-hole-result 3 + proof-goal-with-hole-regexp isar-named-entity-regexp + proof-goal-with-hole-result 2 proof-save-with-hole-regexp nil proof-script-next-entity-regexps isar-next-entity-regexps @@ -227,7 +230,7 @@ See -k option for Isabelle interface script." proof-assistant-setting-format (unless isa-supports-pgip 'isar-markup-ml) - proof-shell-init-cmd '(proof-assistant-settings-cmd) + proof-shell-init-cmd '(proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.restart" proof-shell-eager-annotation-start-length 1 |