diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 04:21:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 04:21:14 +0000 |
| commit | 390a659861192ebf98811438f61c4f992ecad25a (patch) | |
| tree | b730ba7312568eaf620b4096a2af21eb953f9f5e /hol98 | |
| parent | 441b6369abb7863cf65088915cb851ee98f5f59e (diff) | |
New/updated information files
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/README | 21 | ||||
| -rw-r--r-- | hol98/todo | 16 |
2 files changed, 26 insertions, 11 deletions
diff --git a/hol98/README b/hol98/README index 84e4cc5a..a88902f5 100644 --- a/hol98/README +++ b/hol98/README @@ -4,6 +4,14 @@ Written by David Aspinall. $Id$ +Status: not officially supported yet +Maintainer: volunteer required +HOL version: HOL 98, tested with Taupo 2 +HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html + +======================================== + + This is a "technology demonstration" of Proof General for HOL 98. It may work with other versions of HOL, but is untested (please let me @@ -12,16 +20,17 @@ 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 Symbol, 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, maintain and improve it, and thus turn it into a proper instantiation of Proof General. ------------------- -Note: +------------ + +Notes: There are some problems at the moment. HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not @@ -34,8 +43,8 @@ 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 -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). These improvements would be worthwhile contributions to Proof General and also provide the HOL community with a nice front end. @@ -1,12 +1,18 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for HOL -====================== -A Problem with displaying long help message: causes loop in PG +See also ../todo for generic things to do, priority codes. + +** A Problem with displaying long help message: causes loop in PG filtering, why? Process also takes a long time to kill off. -B Improve display to strip ugly val it's. +** B Improve display to strip ugly val it and spurious >'s. + +** B Add special markup to improve robustness + +** B Add support for multiple files + +** B Add support for proof by pointing. + |