diff options
Diffstat (limited to 'hol98/README')
| -rw-r--r-- | hol98/README | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/hol98/README b/hol98/README index 38cbfe26..84e4cc5a 100644 --- a/hol98/README +++ b/hol98/README @@ -6,18 +6,18 @@ $Id$ This is a "technology demonstration" of Proof General for HOL 98. -It may well work with other versions of HOL, but is untested (please -let me know if you try). +It may work with other versions of HOL, but is untested (please let me +know if you try). It has basic script management support, with a little bit of decoration of scripts and output. -There is support for x-symbols, but not using a proper token language. -Try writing "philosophy" ! +There is support for x-symbols, but not using a proper token +language. Try writing "philosophy" ! I have written this in the hope that somebody from the HOL community -will adopt it and turn it into a proper instantiation of -Proof General. +will adopt it, maintain and improve it, and thus turn it into a proper +instantiation of Proof General. ------------------ @@ -25,12 +25,12 @@ Note: There are some problems at the moment. HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not -offer an easy way to edit these kind of proofs. The "Boomburg" Emacs -interface by Koichi Takahashi and Masima Hagiya addressed this, and to -some extent so does the Emacs interface supplied with HOL. Perhaps -one of these could be embedded inside Proof General. Implemented in -a generic way, managing batch vs interactive proofs would also be -useful for Isabelle. +offer an easy way to edit these kind of proofs. The "Boomburg-HOL" +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 would also be useful for Isabelle. Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse |