diff options
Diffstat (limited to 'hol-light/README')
| -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. |