Updated.

3 files changed, 12 insertions, 7 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
diff --git a/twelf/twelf.el b/twelf/twelf.el
index b1b8f1fe..82b32e7e 100644
--- a/twelf/twelf.el
+++ b/twelf/twelf.el
@@ -64,7 +64,10 @@
  ;; or recognize while the prover is pontificating
  proof-shell-eager-annotation-start   
  "^\\[Opening \\|\\[Closing "
- proof-shell-eager-annotation-end "\n")
+ proof-shell-eager-annotation-end "\n"
+
+ ;; next setting is just to prevent warning
+ proof-save-command-regexp	proof-no-regexp)
 
 
 ;; unset: all of the interactive proof commands