diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-10 09:23:33 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-10 09:23:33 +0000 |
| commit | 94308059f0b7a132a902544dbe68142285f379ad (patch) | |
| tree | 661a5c7b30ecd6ff2b364c0d3c49941ab93e9837 /hol98 | |
| parent | 2cce0bc0f772d120b9ad53b9241c78767ac727d0 (diff) | |
Updated
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/README | 24 | ||||
| -rw-r--r-- | hol98/example.sml | 1 |
2 files changed, 13 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 diff --git a/hol98/example.sml b/hol98/example.sml index 04b3b062..64858140 100644 --- a/hol98/example.sml +++ b/hol98/example.sml @@ -7,6 +7,7 @@ g `A /\ B ==> B /\ A`; e DISCH_TAC; e CONJ_TAC; + (* Ooops, I'm stuck now. Can somebody help?? |