diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 08:00:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 08:00:56 +0000 |
| commit | a35b5be37664216deb2afb2ec63009637846d9cc (patch) | |
| tree | 4538f73c11834a06d96b172ffcd12f2098d5582b /hol98 | |
| parent | 4e409735c837314d28f96afa0a7cad9697181fc6 (diff) | |
Updated.
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/README | 12 | ||||
| -rw-r--r-- | hol98/hol98.el | 2 |
2 files changed, 8 insertions, 6 deletions
diff --git a/hol98/README b/hol98/README index 69372fc9..8462763c 100644 --- a/hol98/README +++ b/hol98/README @@ -4,17 +4,17 @@ Written by David Aspinall. Status: not officially supported yet Maintainer: volunteer required -HOL version: HOL98, tested with Taupo 2 -HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html +HOL version: HOL4/HOL98, tested with HOL 4 Kananaskis 2 +HOL homepage: http://hol.sourceforge.net ======================================== -This is a "technology demonstration" of Proof General for HOL 98. +This is a "technology demonstration" of Proof General for HOL4. It may work with other versions of HOL, but is untested (please let me -know if you try). Probably just a few settings need changing -to configure for different output formats. +know if you try). Probably just a few settings need changing to +configure for different output formats. It has basic script management support, with a little bit of decoration of scripts and output. @@ -37,7 +37,7 @@ Emacs interface by Koichi Takahashi and Masima Hagiya addressed this, and to some extent so perhaps does the Emacs interface supplied with HOL. Perhaps one of these could be embedded/reimplemented inside Proof General. Implemented in a generic way, managing batch vs -interactive proofs might also be useful for Isabelle. +interactive proofs might also be useful for other provers. Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse diff --git a/hol98/hol98.el b/hol98/hol98.el index b6cf598b..9990b600 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -62,6 +62,8 @@ ;; proof-shell-eager-annotation-start proof-find-theorems-command "DB.match [] (%s);" + proof-forget-id-command ";" ;; vacuous: but empty string doesn't give + ;; new prompt ;; We must force this to use ptys since mosml doesn't flush its output ;; (on Linux, presumably on Solaris too). proof-shell-process-connection-type t |