diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-24 20:16:22 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-24 20:16:22 +0000 |
| commit | 30d3dd71fe485f9b7a38c1133ec9d2e36a505d46 (patch) | |
| tree | 38e253e8f2c4558b6045b477a87b0e1e8a7b16e0 /hol98 | |
| parent | 2e54ccbf2eabf4b0757d1e0d7f6133906bf913ba (diff) | |
Improved HOL support, now joins together commands in proof properly.
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/hol98.el | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/hol98/hol98.el b/hol98/hol98.el index a11f339a..d2774915 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -21,12 +21,12 @@ proof-comment-end "*)" ;; These are all approximations, of course. proof-goal-command-regexp "^g[ `]" - proof-save-command-regexp nil ;; "^val .*top_thm()" + proof-save-command-regexp "pg_top_thm_and_drop" proof-goal-with-hole-regexp "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove" proof-save-with-hole-regexp "val \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()" proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;" - proof-save-command "val %s = top_thm(); drop();" + proof-save-command "val %s = pg_top_thm_and_drop();" proof-kill-goal-command "drop();" proof-showproof-command "p()" proof-undo-n-times-cmd "(pg_repeat backup %s; p());" @@ -52,7 +52,8 @@ proof-shell-error-regexp "^! " proof-shell-init-cmd "Help.displayLines:=3000; - fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" + fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1)); + fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;" ;; FIXME: add optional help topic parameter to help command. ;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix. proof-info-command "help \"hol\"" @@ -102,6 +103,7 @@ ;; want to duplicate the information here! ;; hol98-keywords '("g" "expand" "e" "val" "store_thm" "top_thm" "by" + "pg_top_thm_and_drop" "Define" "xDefine" "Hol_defn" "Induct" "Cases" "Cases_on" "Induct_on" "std_ss" "arith_ss" "list_ss" |