diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 16:58:54 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 16:58:54 +0000 |
| commit | 2a5709c354e09b06556f3f1e19bf2d9a5ad91564 (patch) | |
| tree | 7c401cc749ec9a5a7ab2fcf127a04eb0ac298b67 /hol98 | |
| parent | b33e3f1c7f799aa3e0f3c70e023fa6a50cb308ad (diff) | |
Updated.
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/README | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hol98/README b/hol98/README index e6c3b4b3..69372fc9 100644 --- a/hol98/README +++ b/hol98/README @@ -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 would also be useful for Isabelle. +interactive proofs might 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 |