Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 22 Mar 1994 16:27:43 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27780; Tue, 22 Mar 1994 09:06:42 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA27771; Tue, 22 Mar 1994 09:01:45 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 22 Mar 1994 16:01:13 +0000 To: info-hol@leopard.cs.byu.edu Subject: Expanded info-hol archive Date: Tue, 22 Mar 94 16:01:04 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:292570:940322160116"@cl.cam.ac.uk> Owing to a generous donation of 58 new messages from Malcolm Newey, the early part of the info-hol archive has been substantially improved. Unfortunately this has led to another change in numbers, so let me encourage people not to refer to messages just by number. Thanks to Phil Windley, the archive can now be browsed with xmosaic. However if anyone wants to access the files explicitly, they reside in: ftp://ftp.cl.cam.ac.uk/hvg/info-hol-archive The files are grouped into hundred-message subdirectories with a gzipped tarfile of each. There is a full index at the top level. Below I give a "concordance" for old and new archive numbers, which also serves to show which new messages have been added. Please let me know of any problems or additional donations. John. OLD# NEW# DATE FROM SUBJECT 0000 0000 30 Aug 88 Phil Windley This mailing list 0001 0001 02 Sep 88 Phil Windley ADD_NORMALIZE_TAC 0002 0002 06 Sep 88 Phil Windley A mailing list for HOL users 0003 0003 06 Sep 88 Michael Russell Re: info-HOL Addition 0004 0004 19 Oct 88 Phil Windley Welcome to info-hol 0005 0005 19 Oct 88 Phil Windley vgrind def for HOL 0006 0006 26 Oct 88 Phil Windley type definitions 0007 0007 27 Oct 88 Tom Melham RE: type definitions 0008 0008 28 Oct 88 Mike Gordon HOL88 0009 0009 13 Nov 88 Mike Gordon HOL88 0010 0010 01 Dec 88 Mike Gordon HOL88 0011 0011 06 Dec 88 Mike Gordon Definitions in HOL88 0012 0012 06 Dec 88 Phil Windley HOL in Common LISP 0013 0013 06 Dec 88 Francisco Corella Formulations of H.O.L. 0014 0014 07 Dec 88 Albert Camilleri HOL in Common Lisp 0015 0015 07 Dec 88 Mike Gordon Forwarding: Re: Forwarding: HOL in Common Lisp 0016 0016 08 Dec 88 David Shepherd HOL in Common Lisp 0017 0017 08 Dec 88 Paul Loewenstein Forwarding: Re: Forwarding: HOL in Common Lisp 0018 0018 09 Dec 88 Mike Gordon SML vs Common Lisp 0019 0019 16 Dec 88 Paul Loewenstein Worries about existential definitions 0020 0020 03 Jan 89 Phil Windley LOOSE DEFINITIONS 0021 09 Feb 89 Phil Windley Bibliography 0022 15 Feb 89 Mike Gordon HOL88 0023 01 Mar 89 Phil Windley Cornell Workshop on Hardware Verification 0024 02 Mar 89 Phil Windley HOL88 is available via ftp 0025 03 Mar 89 Paul Loewenstein Theory of rationals (or reals!)? 0026 06 Mar 89 Paul Loewenstein Franz for SUN OS 0027 06 Mar 89 Phil Windley Franz for SUN OS 0028 07 Mar 89 Phil Windley Bug report: making hol88 on vaxen 0029 07 Mar 89 Paul Loewenstein SUNOS4 and franz-lisp 0021 0030 08 Mar 89 Roger Jones tautologies 0031 09 Mar 89 David Shepherd Franz for SunOS 4 0032 09 Mar 89 Phil Windley HOL88 on Vaxen: bug report 2 0033 09 Mar 89 Phil Windley HOL Version 1.01 0034 10 Mar 89 Paul Loewenstein More arithmetic theorems 0035 31 Mar 89 David Shepherd Conversion package for HOL 0036 04 Apr 89 Miriam Leeser Hardware Workshop to be held at Cornell July 5-7 0037 05 Apr 89 Carlos Delgado Kloos Workshop on Computer-aided Development of Proofs, Theories, Programs, and Circuits 0038 06 Apr 89 Mike Gordon HOL88 news and bug report 0039 06 Apr 89 Phil Windley Hardware Workshop to be held at Cornell July 5-7 0040 17 Apr 89 Mike Gordon Second HOL Users' Meeting 0041 18 Apr 89 Tom Melham hol88 on Vax ULTRIX version 4.2 0042 01 May 89 Phil Windley HOL 88 Feature Report 0043 02 May 89 Mark Stickel CADE Call for Papers 0044 03 May 89 Phil Windley Theory of sets 0045 03 May 89 Paul Loewenstein Theory "sets" inconsistent 0046 08 May 89 Elsa Gunter Theory "sets" 0047 09 May 89 Tom Melham re: predicate representation of sets. 0048 09 May 89 Larry Paulson Classes and Relations in HOL 0049 09 May 89 David Shepherd Re: theory of sets 0050 10 May 89 Andrew Pitts Re: theory of sets 0051 11 May 89 Francisco Corella sets in hol 0052 11 May 89 Thomas Forster 0022 0053 11 May 89 Albert Camilleri Re: theory of sets 0054 12 May 89 Phil Windley 0055 15 May 89 David Shepherd set theory, type defintion, .... 0023 0056 15 May 89 Tom Melham 0057 25 May 89 Mike Gordon Graphs. 0058 25 May 89 Tom Melham 0059 26 May 89 Tom Melham :wordn type definitions in hol 0060 26 May 89 Phil Windley Re: Related to binary word definitions in HOL 0024 0061 26 May 89 Paul Loewenstein Related to binary word definitions in HOL 0025 0062 26 May 89 Phil Windley HOL software available on clover 0026 0063 27 May 89 Tom Melham 0064 28 May 89 Tom Melham some comments on n-bit words 0027 0065 28 May 89 Jeffrey Joyce n-bit words in HOL 0028 0066 29 May 89 Jeffrey Joyce 0029 0067 30 May 89 Paul Loewenstein Yet more on n-bit words in HOL 0030 0068 30 May 89 Paul Loewenstein Dealing with large natural constants. 0031 0069 31 May 89 Roger Jones STRIP_ASSUME_TAC and derivatives 0070 01 Jun 89 Steve Crocker Re: Library for bitstrings 0071 01 Jun 89 Tom Melham Re: recently mentioned problem with STRIP_ASSUME_TAC. 0072 01 Jun 89 Tom Melham ... another similar bug. 0032 0073 02 Jun 89 Tom Melham 0074 02 Jun 89 Mike Gordon A formal verification benchmark 0075 02 Jun 89 Steve Crocker Stumbling over empty bit vectors 0076 02 Jun 89 Paul Loewenstein Left-to-right, right-to-left and zero-length 0077 04 Jun 89 Tom Melham Steve Crocker's theorem... in HOL. 0078 08 Jun 89 Phil Windley HOL88 1.07 is available 0079 29 Jun 89 Phil Windley HOL User's group meeting 0080 30 Jun 89 Mike Gordon HOL Users Meeting 0081 12 Jul 89 Ton Kalker quotient types 0082 12 Jul 89 Ton Kalker quotient package 0083 12 Jul 89 Ton Kalker quotient examples 0084 03 Aug 89 Mike Gordon HOL Meeting 0085 03 Aug 89 Mike Gordon HOL Meeting 0086 09 Aug 89 Mike Gordon Re: info-hol 0087 15 Aug 89 Phil Windley Introduction 0033 0088 17 Aug 89 Phil Windley report on higher-order logic 0034 0089 22 Aug 89 Tom Melham non-compatible changes proposed for type defn package. 0035 0090 25 Aug 89 Phil Windley Re: problem 0036 0091 06 Sep 89 Mike Gordon MacHOL 0037 0092 07 Sep 89 Phil Windley Hardware Verif jobs 0038 0093 14 Sep 89 Paul Loewenstein Kyoto Common Lisp on Sun OS 4.0 0094 18 Sep 89 Luc Claesen Workshop "Applied Formal Methods For Correct VLSI Design" 0095 18 Sep 89 Stig Andur Pedersen HOL mailing list 0039 0096 20 Sep 89 Phil Windley HOL/Emacs interface 0040 0097 20 Sep 89 Phil Windley etags for HOL 0041 0098 20 Sep 89 Phil Windley new franz available 0042 0099 20 Sep 89 Hemendra Talesara Looking for Specific Examples in Architecture Space 0043 0100 10 Oct 89 Mike Gordon HOL Meeting 0044 0101 18 Oct 89 Jing Pan 0045 0102 19 Oct 89 Tim Leonard Floating-point verification 0046 0103 24 Oct 89 Ramayya Kumar Teething Troubles with HOL 0047 0104 25 Oct 89 Phil Windley Re: Teething Troubles with HOL 0048 0105 25 Oct 89 Phil Windley REWRITING WITH TRUTH 0049 0106 26 Oct 89 Tom Melham sticky types in HOL88 0050 0107 26 Oct 89 Amit Jasuja type abbreviations in HOL 0051 0108 27 Oct 89 Mike Gordon Re: type abbreviations in HOL 0052 0109 31 Oct 89 Mike Gordon HOL Meeting 0053 0110 13 Nov 89 Richard Boulton 0054 0111 21 Nov 89 Mike Gordon HOL Meeting 0055 0112 22 Nov 89 Phil Windley association lists in HOL 0056 0113 23 Nov 89 Mike Gordon Forwarding: WOW 0057 0114 29 Nov 89 Tom Melham new_recursive_definition 0058 0115 06 Dec 89 Mike Gordon HOL dinner 0059 0116 06 Dec 89 Tom Melham an inconsistent axiom for lists. 0060 0117 07 Dec 89 Andy Pitts Re: an inconsistent axiom for lists. 0061 0118 07 Dec 89 Paul Loewenstein Lists with elements of varying types 0119 07 Dec 89 Paul Loewenstein Lists with elements of varying types 0062 0120 08 Dec 89 Mike Gordon Documentation 0063 0121 19 Dec 89 Phil Windley bug fix for HOL88 1.11 0064 0122 20 Dec 89 Phil Windley HOL88 ver 1.11 0065 0123 30 Dec 89 Phil Windley HOL Documentation 0066 0124 08 Jan 90 John Van Tassel HOL niftp availability 0067 0125 13 Jan 90 Phil Windley Ultrix and make 0068 0126 13 Jan 90 Mike Gordon Apple Macintosh prices to run HOL 0069 0127 16 Jan 90 Tom Melham using FIRST_ASSUM in your tactic proofs. 0070 0128 16 Jan 90 Michael Wirth Speed of Lisp systems on the Macintosh .... (and thereafter \n. n + 58)