From 5d6827b0fbdd14fdc65cb3a20453a265d0947be3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 10 Oct 2010 22:08:17 +0000 Subject: Updated --- hol-light/README | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) (limited to 'hol-light') 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. -- cgit v1.2.3