From 05259143d11796175d84535bbe3211ea963b4cf9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 19 Jan 2012 12:48:02 +0000 Subject: Update documentation --- hol-light/LICENSE-HOL-LIGHT | 29 +++++++++++++++++++++++++++++ hol-light/README | 16 ++++++++-------- 2 files changed, 37 insertions(+), 8 deletions(-) create mode 100644 hol-light/LICENSE-HOL-LIGHT (limited to 'hol-light') 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. -- cgit v1.2.3