diff options
| author | David Aspinall | 2000-03-10 06:57:31 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-03-10 06:57:31 +0000 |
| commit | ce1de45404de06e971d1bcb8a00c33292544cc14 (patch) | |
| tree | 212c3f7b98c9934aa65eba9a98b98df9fa5d57d6 /html | |
| parent | 6ab6ee50b10c3ae408e8e04a84966c696ee628ff (diff) | |
Updated
Diffstat (limited to 'html')
| -rw-r--r-- | html/projects/hol.html | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/html/projects/hol.html b/html/projects/hol.html index 80e9e208..4b623bfb 100644 --- a/html/projects/hol.html +++ b/html/projects/hol.html @@ -11,18 +11,19 @@ Much more than Isabelle, HOL relies on its meta language, ML. HOL proof scripts often use batch-oriented single step tactic proofs constructed in ML, but Proof General does not offer an easy way to edit these kind of proofs (as opposed to multi-step interactive -proofs). The "Boomburg" Emacs interface by Koichi Takahashi and -Masima Hagiya addressed this problem, as well as providing support for -proof-by-pointing to HOL. Their interface (which is no longer -maintained) could perhaps be embedded or reimplemented inside Proof -General. Implemented in a generic way, batch script editing would -also be useful for Isabelle. +proofs). The <a +href="http://hagi.is.s.u-tokyo.ac.jp/boomborg/">Boomburg-HOL</a> Emacs +interface by Koichi Takahashi and Masima Hagiya addressed this +problem, as well as providing support for proof-by-pointing to HOL. +Their interface could perhaps be reinterpreted or reimplemented inside +Proof General. Implemented in a generic way, batch script editing +would also be useful for Isabelle. </p> <p> Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse -SML, it just looks for semicolons. Again, this could be improved by -taking a better parser (e.g. from sml mode). +SML, it just looks for semicolons. This could be improved by taking a +better parser (e.g. from sml mode). </p> <p> <b>Skills:</b> |