Update documentation

1 files changed, 29 insertions, 0 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.