Update documentation

2 files changed, 37 insertions, 8 deletions

diff --git a/hol-light/LICENSE-HOL-LIGHT b/hol-light/LICENSE-HOL-LIGHT
new file mode 100644
index 00000000..f192eff1
--- /dev/null
+++ b/hol-light/LICENSE-HOL-LIGHT
@@ -0,0 +1,29 @@
+            HOL Light copyright notice, licence and disclaimer
+
+                     (c) University of Cambridge 1998
+                  (c) Copyright, John Harrison 1998-2008
+
+HOL Light version 2.20, hereinafter referred to as "the software", is a
+computer theorem proving system written by John Harrison. Much of the
+software was developed at the University of Cambridge Computer Laboratory,
+New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England. The
+software is copyright, University of Cambridge 1998 and John Harrison
+1998-2007.
+
+Permission to use, copy, modify, and distribute the software and its
+documentation for any purpose and without fee is hereby granted. In the
+case of further distribution of the software the present text, including
+copyright notice, licence and disclaimer of warranty, must be included in
+full and unmodified form in any release. Distribution of derivative
+software obtained by modifying the software, or incorporating it into
+other software, is permitted, provided the inclusion of the software is
+acknowledged and that any changes made to the software are clearly
+documented.
+
+John Harrison and the University of Cambridge disclaim all warranties
+with regard to the software, including all implied warranties of
+merchantability and fitness. In no event shall John Harrison or the
+University of Cambridge be liable for any special, indirect,
+incidental or consequential damages or any damages whatsoever,
+including, but not limited to, those arising from computer failure or
+malfunction, work stoppage, loss of profit or loss of contracts.
diff --git a/hol-light/README b/hol-light/README
index 34c32e32..59356fb7 100644
--- a/hol-light/README
+++ b/hol-light/README
@@ -1,18 +1,18 @@
 HOL Light in Proof General.
 
-Written by David Aspinall.
+Written by David Aspinall and Mark Adams.
 
 Status:	           not officially supported yet
 Maintainer:        volunteer required
-HOL-Light version: 
-HOL homepage:      http://hol.sourceforge.net
+HOL-Light version: SVN trunk (a moving target 8-) - tested on 118)
+HOL homepage:      https://www.cl.cam.ac.uk/~jrh13/hol-light/
 
 ========================================
 
 
 This is a "technology demonstration" of Proof General for HOL-Light.
 
-I have written this in the hope that somebody from the HOL-Light
+We 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.
 
@@ -30,10 +30,10 @@ 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).
+Another problem is that HOL scripts sometimes use OCaml modules, which
+will cause confusion because Proof General does not really parse OCaml,
+it just looks for semicolons.  This could be improved by taking a
+better parser (perhaps from the OCaml mode for Emacs).
 
 These improvements would be worthwhile contributions to Proof General
 and also provide the HOL community with a nice front end.