From c6dc09f3633aa500c6f0d2924f5effd5e734d8ac Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 29 Sep 2010 12:15:41 +0000
Subject: Experimental hol-light version, not usable yet

---
 hol-light/README | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 hol-light/README

(limited to 'hol-light/README')

diff --git a/hol-light/README b/hol-light/README
new file mode 100644
index 00000000..edcba896
--- /dev/null
+++ b/hol-light/README
@@ -0,0 +1,53 @@
+HOL Light in Proof General.
+
+Written by David Aspinall.
+
+Status:	           not officially supported yet
+Maintainer:       volunteer required
+HOL-Ligh version:
+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.
+
+
+------------
+
+Notes:
+
+There are some problems at the moment.  HOL proof scripts often use
+batch-oriented single step tactic proofs, but Proof General does not
+offer an easy way to edit these kind of proofs.  The "Boomburg-HOL"
+Emacs interface by Koichi Takahashi and Masima Hagiya addressed this,
+and to some extent so perhaps does the Emacs interface supplied with
+HOL.  Perhaps one of these could be embedded/reimplemented inside
+Proof General.  Implemented in a generic way, managing batch vs
+interactive proofs might also be useful for other provers.
+
+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.  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.  
+Please have a go!
+
+
+$Id$
+
-- 
cgit v1.2.3