diff options
Diffstat (limited to 'hol-light/README')
| -rw-r--r-- | hol-light/README | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/hol-light/README b/hol-light/README index 59356fb7..238586c6 100644 --- a/hol-light/README +++ b/hol-light/README @@ -24,11 +24,12 @@ Notes: 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-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 might also be useful for other provers. +Emacs interface by Koichi Takahashi and Masima Hagiya addressed this a +long time ago, 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 +other provers. Another problem is that HOL scripts sometimes use OCaml modules, which will cause confusion because Proof General does not really parse OCaml, |