Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 7 Dec 1992 19:22:45 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05541; Mon, 7 Dec 92 10:58:31 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05529; Mon, 7 Dec 92 10:58:05 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Mon, 7 Dec 1992 18:57:14 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Dynamically FTPable "contrib" Date: Mon, 07 Dec 92 18:57:09 +0000 From: John Harrison Message-Id: <"nene.cl.ca.575:07.12.92.18.57.16"@cl.cam.ac.uk> It has been decided that from now on, the "contrib" area that we keep at Cambridge (for the code people send us for inclusion in HOL) will be available for FTP dynamically, i.e. new entries or changes will be accessible between HOL releases. The details are: ftp.cl.cam.ac.uk [128.232.0.56] in directory "hvg/contrib" The subdirectories are all in their "unpacked" form, so in general you may need to get several files from inside them. Below is a list, in chronological order where dates are known, of the current subdirectories and a summary of their contents. Today's HOL 2.01 release contains all these, except the last two (WF and bugfixes) which have been added since HOL was packaged up for FTP. People are welcome to continue sending code for contrib (preferably to "hol-support@cl.cam.ac.uk", otherwise to me personally) in the expectation that it will appear here shortly after. Regards, John Harrison (jrh@cl.cam.ac.uk) Hardware Verification Group University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG England. Phone: +44 223 334760 Fax: +44 223 334678 ============================================================================= DATE DIRECTORY CONTENTS ^^^^^^ ^^^^^^^^^^^ ^^^^^^^^^^ ??.??.?? hol-errors Interpretations of various HOL errors and how to fix them (sometimes). [Phil Windley] ??.??.?? mut_rec_types Defining mutually recursive types in HOL. [Peter Strarup Jensen, Ann-Grete Tan & Anders Pilegaard] ??.??.?? v11_lib Version 1.11 libraries: card, well_order, zet, csp [N/A] ??.??.?? wordn Theory of n-bit words. [Wai Wong] 89.??.?? hol-mode Emacs HOL (Higher Order Logic) Mode. [Kim Dam Petersen] 89.03.30 icl-taut Various theorem proving utilities, including a tautology checker. [R.B.Jones] 90.04.11 PNF Conversions to reduce terms to prenex normal form. [Clive Jervis] 90.04.11 batch-hol-tool Batch HOL session with merged input and output. [Richard Boulton] 90.04.11 franz-cl-th Unix script for translating theory files from Franz to common lisp. [John Carroll] 90.04.11 knuth-bendix Knuth Bendix completion as a derived inference rule. [Konrad Slind] 90.04.11 tooltool SunView HOL interface tool (using tooltool). [David Shepherd] 90.04.20 select Note on dealing with the epsilon-operator in HOL proofs. [Brian Graham] 90.06.01 CPO Basic theory of CPO's and fixed-points. [Albert J. Camilleri] 90.08.03 temporal Temporal logic in HOL. [Amit Jasuja] 90.11.14 rewriting Rewriting tools. [R. A. Fleming] 90.12.12 subgoal Experimental new subgoal package [R. A. Fleming] 90.12.14 latex LaTeX macros for typesetting HOL. [Jim Alves-Foss] 91.01.?? hol-emacs A simple interface for running HOL under the GNU Emacs editor. [Phil Windley] 91.01.20 hol_users Information on groups using HOL. [Sara Kalvala] 91.01.25 btg-tactics Extra general-purpose tactics. [Brian Graham] 91.01.27 tex-thy-format Format a HOL theory in LaTeX format. [Wai Wong] 91.01.28 benchmark The HOL "multiplier" benchmark (for version 1.12). [Mike Gordon] 91.08.?? koenig A proof of Koenig's Lemma. [Paul Loewenstein] 91.08.21 prooftree Enhanced subgoal package. [Sara Kalvala] 92.02.27 SECD The SECD microprocessor specification and verification. [Brian Graham] 92.03.02 holsort Sorts files of axioms, etc., or of typed constants. [Stephen H. Brackin] 92.06.18 non-unix Instructions for making HOL on non-UNIX machines. [John Carroll] 92.08.?? res_quan Library for dealing with restricted quantifiers. [Wai Wong] 92.08.26 Xhelp Xwindows browser for HOL documentation. [Sara Kalvala] 92.09.01 rule-induction Examples using the inductive definitions package. [Juanito Camilleri & Tom Melham] 92.09.18 hol-sum Summary of HOL system Version 2. [Wai Wong] 92.10.06 aci Generalizing AC operation with identity to finite sets. [Ching-Tsun Chou] 92.10.06 cont Interactive Theorem Proving with Theorem Continuation Functions. [Ching-Tsun Chou] 92.10.06 pred A Sequent Formulation of a Logic of Predicates in HOL. [Ching-Tsun Chou] 92.10.07 hol-exec HOLER: The HOL Evaluator [Sreeranga Rajan] 92.10.16 boyer-moore Boyer-Moore Automation for HOL. [Richard J. Boulton] 92.10.25 fpf A theory of finite partial functions (finite maps). [Donald Syme] 92.10.25 smarttacs Several general purpose tactics. [Donald Syme] 92.10.29 Tarski Definition of a theory for defining recursive boolean functions. [Flemming Andersen & Kim Dam Petersen] 92.10.?? newrw Updates rewriting conversions in HOL2.0 code to HOL2.01 [Jim Grundy] 92.11.04 prog_logic92 Program semantics inc. (unbounded) nondeterminism, total correctness. [Gavan Tredoux] 92.11.25 make_use Automatically generates autoloading commands for a theory. [Donald Syme] 92.12.01 AKCL-mods A hol-init file to increase the speed of HOL when built under AKCL. [John Van Tassel] 92.12.04 WF Theory of well founded relations. [Wishnu Prasetya] 92.12.05 bugfixes Bug fixes since last release of HOL. [hol-support]