diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-10-10 22:08:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-10-10 22:08:17 +0000 |
| commit | 5d6827b0fbdd14fdc65cb3a20453a265d0947be3 (patch) | |
| tree | c67350e451d10fc3b77442fbaadb62d092d80d7f /hol-light | |
| parent | 26dbf751f71a9a47fa70d43763604356a8b052a0 (diff) | |
Updated
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/README | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/hol-light/README b/hol-light/README index edcba896..34c32e32 100644 --- a/hol-light/README +++ b/hol-light/README @@ -3,8 +3,8 @@ HOL Light in Proof General. Written by David Aspinall. Status: not officially supported yet -Maintainer: volunteer required -HOL-Ligh version: +Maintainer: volunteer required +HOL-Light version: HOL homepage: http://hol.sourceforge.net ======================================== @@ -12,15 +12,6 @@ HOL homepage: http://hol.sourceforge.net This is a "technology demonstration" of Proof General for HOL-Light. -It may work with other versions of HOL, but is untested (please let me -know if you try). Probably just a few settings need changing to -configure for different output formats. - -It has basic script management support, with a little bit of -decoration of scripts and output. - -There is support for Unicode Tokens. - I have written this in the hope that somebody from the HOL-Light community will adopt it, maintain and improve it, and thus turn it into a proper instantiation of Proof General. |