Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <02515-0@swan.cl.cam.ac.uk>; Mon, 3 Aug 1992 21:16:38 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14653; Mon, 3 Aug 92 12:56:58 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA14648; Mon, 3 Aug 92 12:56:25 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <02363-0@swan.cl.cam.ac.uk>; Mon, 3 Aug 1992 20:55:01 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Archive of info-hol Date: Mon, 03 Aug 92 20:54:56 +0100 From: John Harrison Message-Id: <"swan.cl.ca.365:03.07.92.19.55.04"@cl.cam.ac.uk> Victor mentioned my info-hol archive in his previous message. I've added the message it was missing, but there are no doubt lots of other errors or omissions, particularly before I was put on the list myself (about March 1991). I therefore thought I would send a list of the messages I have (I expect the one-line summaries will be enough to specify them), in the hope that other members of the mailing list might be able to fill some holes. I'd be grateful for any old messages people can find. I intend to make the archive available for FTP in due course. John. (jrh@cl.cam.ac.uk) P.S. I hope I haven't got too many peoples' names wrong... 001 30 Aug 88 Phil Windley This mailing list 002 02 Sep 88 Phil Windley ADD_NORMALIZE_TAC 003 06 Sep 88 Phil Windley A mailing list for HOL users 004 06 Sep 88 Michael Russell Re: info-HOL Addition 005 19 Oct 88 Phil Windley Welcome to info-hol 006 19 Oct 88 Phil Windley vgrind def for HOL 007 26 Oct 88 Phil Windley type definitions 008 27 Oct 88 Tom Melham RE: type definitions 009 28 Oct 88 Mike Gordon HOL88 010 13 Nov 88 Mike Gordon HOL88 011 01 Dec 88 Mike Gordon HOL88 012 06 Dec 88 Mike Gordon Definitions in HOL88 013 06 Dec 88 Phil Windley HOL in Common LISP 014 06 Dec 88 Francisco Corella Formulations of H.O.L. 015 07 Dec 88 Albert Camilleri HOL in Common Lisp 016 07 Dec 88 Mike Gordon Forwarding: Re: Forwarding: HOL in Common Lisp 017 08 Dec 88 David Shepherd HOL in Common Lisp 018 08 Dec 88 Paul Loewenstein Forwarding: Re: Forwarding: HOL in Common Lisp 019 09 Dec 88 Mike Gordon SML vs Common Lisp 020 16 Dec 88 Paul Loewenstein Worries about existential definitions 021 03 Jan 89 Phil Windley LOOSE DEFINITIONS 022 08 Mar 89 Roger Jones tautologies 023 11 May 89 Albert Camilleri Re: theory of sets 024 15 May 89 Tom Melham 025 26 May 89 Paul Loewenstein Related to binary word definitions in HOL 026 26 May 89 Phil Windley HOL software available on clover 027 27 May 89 Tom Melham 028 28 May 89 Jeffrey Joyce n-bit words in HOL 029 29 May 89 Jeffrey Joyce 030 30 May 89 Paul Loewenstein Yet more on n-bit words in HOL 031 30 May 89 Paul Loewenstein Dealing with large natural constants. 032 31 May 89 Roger Jones STRIP_ASSUME_TAC and derivatives 033 02 Jun 89 Tom Melham 034 17 Aug 89 Phil Windley report on higher-order logic 035 22 Aug 89 Tom Melham non-compatible changes proposed for type defn package. 036 25 Aug 89 Phil Windley Re: problem 037 06 Sep 89 Mike Gordon MacHOL 038 07 Sep 89 Phil Windley Hardware Verif jobs 039 14 Sep 89 Paul Loewenstein Kyoto Common Lisp on Sun OS 4.0 040 20 Sep 89 Phil Windley HOL/Emacs interface 041 20 Sep 89 Phil Windley etags for HOL 042 20 Sep 89 Phil Windley new franz available 043 20 Sep 89 Hemendra Talesara Looking for Specific Examples in Architecture Space 044 10 Oct 89 Mike Gordon HOL Meeting 045 18 Oct 89 Jing Pan 046 19 Oct 89 Tim Leonard Floating-point verification 047 24 Oct 89 Ramayya Kumar Teething Troubles with HOL 048 25 Oct 89 Phil Windley Re: Teething Troubles with HOL 049 25 Oct 89 Phil Windley REWRITING WITH TRUTH 050 26 Oct 89 Tom Melham sticky types in HOL88 051 26 Oct 89 Amit Jasuja type abbreviations in HOL 052 27 Oct 89 Mike Gordon Re: type abbreviations in HOL 053 31 Oct 89 Mike Gordon HOL Meeting 054 13 Nov 89 Richard Boulton 055 21 Nov 89 Mike Gordon HOL Meeting 056 22 Nov 89 Phil Windley association lists in HOL 057 23 Nov 89 Mike Gordon Forwarding: WOW 058 29 Nov 89 Tom Melham new_recursive_definition 059 06 Dec 89 Mike Gordon HOL dinner 060 06 Dec 89 Tom Melham an inconsistent axiom for lists. 061 07 Dec 89 Andy Pitts Re: an inconsistent axiom for lists. 062 07 Dec 89 Paul Loewenstein Lists with elements of varying types 063 08 Dec 89 Mike Gordon Documentation 064 19 Dec 89 Phil Windley bug fix for HOL88 1.11 065 20 Dec 89 Phil Windley HOL88 ver 1.11 066 30 Dec 89 Phil Windley HOL Documentation 067 08 Jan 90 John Van Tassel HOL niftp availability 068 13 Jan 90 Phil Windley Ultrix and make 069 13 Jan 90 Mike Gordon Apple Macintosh prices to run HOL 070 16 Jan 90 Tom Melham using FIRST_ASSUM in your tactic proofs. 071 16 Jan 90 Michael Wirth Speed of Lisp systems on the Macintosh 072 17 Jan 90 DCC Workshop Oxford Workshop on Designing Correct Circuits -- Call for Papers 073 18 Jan 90 John Carroll HOL ported to Macintosh Allegro CL 074 20 Jan 90 Tom Melham another remark about FIRST_ASSUM. 075 10 Feb 90 Phil Windley lisps 076 11 Feb 90 John Carroll Re: lisps 077 13 Feb 90 Mark Bouler Tactics for arithmetical reasoning 078 16 Feb 90 Phil Windley 1989 User's Group Meeting Abstracts (1 of 2) 079 16 Feb 90 Phil Windley 1989 User's Group Meeting Abstracts (2 of 2) 080 18 Feb 90 Wim Ploegaerts Allegro Common Lisp on DEC 3100 081 20 Feb 90 Mark Woodcock Sun Common 3.0 082 22 Feb 90 Mike Gordon Getting HOL documentation 083 23 Feb 90 Wai Wong 084 23 Feb 90 Mike Gordon 085 28 Feb 90 Phil Windley HOL 90 086 28 Feb 90 Jeffrey Joyce running HOL on Apollo's 087 01 Mar 90 Ton Kalker Re: running HOL on Apollo's 088 06 Mar 90 Jeffrey Joyce 1990 HOL Users Group Meeting 089 15 Mar 90 Steven Bancroft HOL build problem 090 16 Mar 90 Mike Gordon HOL news 091 16 Mar 90 Phil Windley HOL90: call for votes 092 19 Mar 90 Ann Grete Tan HOL90 - Aarhus University, Denmark 093 22 Mar 90 Mike Gordon Positions available at Cambridge 094 22 Mar 90 Ann Grete Tan HOL90 - Aarhus University, Denmark 095 26 Mar 90 Jeffrey Joyce HOL Course at UBC, June 4-8 096 27 Mar 90 Per Hasle 097 30 Mar 90 Mike Gordon New HOL interface 098 02 Apr 90 Ramayya Kumar Trouble in creating Libraries for Version 1.11 099 03 Apr 90 Phil Windley Last call for votes 100 04 Apr 90 Robin Sharp Re: Last call for votes 101 04 Apr 90 Josh Guttman HOL for mathematics? 102 05 Apr 90 Flemming Andersen Re: Trouble in creating Libraries for Version 1.11 103 06 Apr 90 Josh Guttman Semantics: Full or general? 104 06 Apr 90 Franscisco Corella Semantics of HOL 105 09 Apr 90 Andy Pitts Re: Semantics of HOL 106 10 Apr 90 Dave Barker-Plummer A Question Regarding REWRITE_TAC and its friends. 107 12 Apr 90 Tom Melham Some remarks on REWRITE_TAC in answer to the question. 108 13 Apr 90 Phil Windley a note on building HOL 109 14 Apr 90 Phil Windley HOL Error Interpretations 110 15 Apr 90 Mike Gordon HOL Error Interpretations 111 17 Apr 90 Al Stavely need help with MATCH_MP_IMP_TAC 112 18 Apr 90 Tom Melham MATCH_MP_IMP_TAC. 113 19 Apr 90 Ramayya Kumar HOL-Novice needs help! 114 19 Apr 90 Brian Graham re: HOL-Novice needs help! 115 19 Apr 90 Brian Graham Choice operator in HOL88 116 19 Apr 90 Tom Melham dealing with epsilon... 117 20 Apr 90 Phil Windley Brian's paper 118 21 Apr 90 Mike Gordon Congratulations to Oxford and INMOS 119 24 Apr 90 Mark Stickel CADE-10 Schedule and Registration Form 120 24 Apr 90 Phil Windley HOL 90 121 24 Apr 90 Jeffrey Joyce HOL Course at UBC, Vancouver (Reminder) 122 25 Apr 90 Jing Pan 123 27 Apr 90 Neil Viljoen Subscription 124 30 Apr 90 Mike Gordon Names and addresses wanted 125 01 May 90 Wai Wong MATCH_MP_IMP_TAC 126 04 May 90 Jim Alves-Foss SPECing simple polymorphic types 127 05 May 90 Tom Melham RE: SPECing simple polymorphic types 128 09 May 90 Larry Paulson Isabelle available by FTP 129 10 May 90 Glynn Winskel Date of the HOL90 meeting 130 10 May 90 Brian Graham re: dealing with choice operator 131 10 May 90 Steven Bancroft HOL build prob. w/ SUN CL 3.0.4 132 23 May 90 Ramayya Kumar Temporal Operators 133 23 May 90 Sara Kalvala Recursion in HOL 134 23 May 90 Amit Jasuja Re: Temporal Operators 135 25 May 90 Albert Camilleri Defining recursive operators. 136 25 May 90 Pim Kars 137 27 May 90 Tom Melham MOD and DIV in HOL88 version 1.12 138 28 May 90 Mike Gordon definitions 139 13 Jun 90 Testing, 140 15 Jun 90 Kim Dam Petersen Error in AUTO_SPECL (of Elsa Gunther) 141 16 Jun 90 Dave Barker-Plummer definitions 142 20 Jun 90 Glynn Winskel International HOL meeting 143 21 Jun 90 Flemming Andersen RO 144 27 Jun 90 Dave Barker-Plummer Missing Makefile for Isabelle? 145 12 Jul 90 Todd Fine info-hol mailing list 146 15 Jul 90 DCC Workshop Workshop on Designing Correct Circuits, Oxford, 26--28 September 1990 147 16 Jul 90 Claude Fleurey Mailing list for HOL users 148 25 Jul 90 Phil Windley machines and hol 149 25 Jul 90 Phil Windley AKCL and SparcStations 150 26 Jul 90 Tom Melham all_sets library : revision and contributions 151 27 Jul 90 Phil Windley Exit 137 152 27 Jul 90 Phil Windley VIPER info from COMP.RISKS 153 30 Jul 90 Ramayya Kumar Definition of turnstile operator 154 31 Jul 90 Mike Gordon Job advertisement. 155 31 Jul 90 Tom Melham all_sets library (re-posting) 156 03 Aug 90 Tom Melham temporal operators can't be truth functional 157 06 Aug 90 Glynn Winskel HOL USERS MEETING 158 16 Aug 90 Wim Ploegaerts 159 17 Aug 90 Joakim von Wright Help needed with MacHOL 160 20 Aug 90 Kim Dam Petersen About the choice and existence operator 161 21 Aug 90 Kim Dam Petersen About the choice and existence operator 162 22 Aug 90 Kim Dam Petersen Problems with new_recursive_definition 163 22 Aug 90 (JUNK) Pls. remove me from the mailing list. 164 23 Aug 90 Tom Melham RE: problem with new_recursive_definition. 165 25 Aug 90 Paul Loewenstein National Semiconductor 166 27 Aug 90 Maris Ozols |info-hol mailing list| 167 27 Aug 90 Maris Ozols info-hol mailing list 168 31 Aug 90 Phil Windley retransmit 169 06 Sep 90 Glynn Winskel HOL meeting---a correction 170 18 Sep 90 Glynn Winskel PROGRAMME FOR HOL MEETING 171 18 Sep 90 Josh Guttman Re: Programme for HOL meeting 172 21 Sep 90 Carsten Rickers HOL Meeting 173 25 Sep 90 Anders Pilegaard HOL meeting --- abstracts available 174 18 Oct 90 Ramayya Kumar Need help creating a Sparc version using Sun CL 3.0.0 175 31 Oct 90 Phil Windley HOL running times on Apollo's vs SPARC's 176 02 Nov 90 is e-mail address ok? 177 08 Nov 90 Luc Claesen ACM International Workshop on Formal Methods in VLSI Design 178 12 Nov 90 Sandy Murphy primitive recursive functions 179 12 Nov 90 Sandy Murphy recursive functions 180 13 Nov 90 Josh Guttman Re: primitive recursive functions 181 13 Nov 90 Phil Windley RE: primitive recursive functions 182 26 Nov 90 Avra Cohn HOL Users Group Mtg 1991 183 06 Dec 90 Sara Kalvala projects using HOL 184 10 Dec 90 Jim Alves-Foss LaTeX macros for HOL --> logic 185 11 Dec 90 Phil Windley Research Assistantships in Formal Methods 186 12 Dec 90 Elsa Gunter 187 14 Dec 90 Sandy Murphy graph theory available? 188 18 Dec 90 Flemming Andersen Re: projects using HOL 189 30 Dec 90 Jeffrey Joyce HOL COURSE - April 1991 - Vancouver, Canada 190 08 Jan 91 Avra Cohn HOL Users Group Mtg 1991 191 08 Jan 91 Jim Alves-Foss Re: HOL Users Group Mtg 1991 192 09 Jan 91 Inder Dhingra Re: HOL Users Group Mtg 1991 193 14 Jan 91 Mark Heckman add to list 194 15 Jan 91 Sara Kalvala Re: projects using HOL 195 15 Jan 91 Jim Alves-Foss Re: projects using HOL 196 21 Jan 91 Avra Cohn HOL Users Group Mtg 1991 197 23 Jan 91 Tom Melham version 12 contrib directory 198 25 Jan 91 Anders Pilegaard Defining mutually recursive types in HOL 199 25 Jan 91 Jeffrey Joyce TPCD 92 - Call for papers 200 28 Jan 91 J Staunstrup Call for Papers - DCC 92 201 28 Jan 91 Mike Fourman Another Conference 202 28 Jan 91 Mike Fourman DCC-92 Call for papers 203 28 Jan 91 Paul Loewenstein Theorem proving vs. Domain-specific tools. 204 28 Jan 91 Phil Windley VACANCY ANNOUNCEMENT 205 29 Jan 91 Avra Cohn HOL Users Group Mtg 1991 206 29 Jan 91 Wim Ploegaerts hol-akcl 207 30 Jan 91 Wim Ploegaerts hol-akcl 208 30 Jan 91 Glynn Winskel Invoices 209 07 Feb 91 Mark van de Voort 210 21 Feb 91 Jim Alves-Foss Re: Security 211 21 Feb 91 Tony Cant String to term conversion 212 21 Feb 91 Tony Cant Security 213 28 Feb 91 Sara Kalvala HOL 1.12 is out! 214 28 Feb 91 John Van-Tassel Re: String to term conversion 215 04 Mar 91 Sara Kalvala HOL 1.12 release 216 05 Mar 91 Neil Murray CADE-11 217 07 Mar 91 Sara Kalvala hol tar files 218 11 Mar 91 Phil Windley HOL now available by FTP 219 11 Mar 91 Mike Simon 220 12 Mar 91 Mike Gordon Position available at Cambridge 221 14 Mar 91 Ramayya Kumar Problems installing HOL 1.12 222 15 Mar 91 Phil Windley HOL112 fix for Lucid CL 223 18 Mar 91 Jon Jacky HOL and control systems? 224 21 Mar 91 Josh Guttman semantics of polymorphic operators 225 22 Mar 91 Mike Fourman Re: semantics of polymorphic operators 226 22 Mar 91 Rob Arthan 227 25 Mar 91 Mike Fourman Re: semantics of polymorphic operators 228 25 Mar 91 Mike Fourman Whoops! Correction Re: semantics of polymorphic operators 229 26 Mar 91 Elsa Gunter 230 29 Mar 91 Jeffrey Joyce "why h.o.l. ?" 231 01 Apr 91 Josh Guttman Re: semantics of polymorphic operators 232 02 Apr 91 Phil Windley HOL on a DS5000 using AKCL 233 03 Apr 91 Andrew Pitts Re: semantics of polymorphic operators 234 04 Apr 91 Paul Curzon Theories of Lists 235 08 Apr 91 Jim Alves-Foss Ports of HOL to different architecutres and Lisp implementations? 236 09 Apr 91 Wim Ploegaerts Re: Ports of HOL to different architecutres and Lisp implementations? 237 09 Apr 91 John Van-Tassel Re: Ports of HOL to different architecutres and Lisp implementations? 238 10 Apr 91 Phil Windley Re: help with a reference 239 10 Apr 91 Jeffrey Joyce help with a reference 240 10 Apr 91 Myla Archer 1991 HOL Workshop 241 11 Apr 91 Phil Windley Re: bit manipulation 242 11 Apr 91 bit manipulation 243 15 Apr 91 Mike Gordon New HOL hacker 244 16 Apr 91 Thomas Forster Re: New HOL hacker 245 16 Apr 91 Flemming Andersen Re: New HOL hacker 246 19 Apr 91 Phil Windley lattices 247 19 Apr 91 Tom Melham Re: bit manipulation 248 22 Apr 91 Tim Redmond HOL on a 386 (Sys V Unix) 249 25 Apr 91 Damir Jamsek Trying to Build HOL1.12, sun3, SunOS4.x, AKCL 1.530 250 25 Apr 91 Phil Windley save_thm and hypostheses/ abstract theories 251 27 Apr 91 Mike Gordon save_thm problem 252 27 Apr 91 Tom Melham saving theorems with hypotheses. 253 01 May 91 Phil Windley info-hol and Clover 254 02 May 91 Luc Claesen The European Conference on Design Automation 255 02 May 91 Sally Goodall CADE-11 256 06 May 91 Sally Goodall CADE 11 257 17 May 91 Victor Carreno registration fee 258 20 May 91 Tim Leonard Digital fellowship 259 21 May 91 Jeffrey Joyce Travel Bursaries for HOL Meeting in Davis 260 22 May 91 Roger Jones ICL Z Proof tool and formal specs of HOL 261 31 May 91 Tom Melham Formal methods awareness club. 262 04 Jun 91 Sara Kalvala survey of applications 263 04 Jun 91 Wai Wong problem in building HOL on a sun4 using AKCL 264 06 Jun 91 Phil Windley HOL91 265 13 Jun 91 Graham Birtwistle 266 17 Jun 91 Todd Fine HOL on a Mac 267 17 Jun 91 Garrel Pottinger Questions about the HOL logic 268 20 Jun 91 Phil Windley mail problems 269 20 Jun 91 Phil Windley HOL User's Group Meeting Travel Bursaries 270 20 Jun 91 Sandy Murphy select 271 21 Jun 91 Paul Loewenstein select 272 21 Jun 91 David Shepherd Re: select 273 27 Jun 91 Rob Arthan select 274 27 Jun 91 Roger Jones A response to "select" (on use of the choice function) 275 15 Jul 91 Tom Schubert 276 23 Jul 91 Sandy Murphy Re: select 277 25 Jul 91 Josh Guttman Semantics of select 278 26 Jul 91 Roger Jones More on the choice function 279 26 Jul 91 Josh Guttman Re: More on the choice function 280 27 Jul 91 Ian Sutherland Re: More on the choice function 281 29 Jul 91 Phil Windley latex macros that IEEE didn't send 282 29 Jul 91 Mike Gordon Select operator (practical perspective) 283 29 Jul 91 Roger Jones A final word on choice? 284 29 Jul 91 Rob Arthan Choice 285 30 Jul 91 Josh Guttman Re: More on the choice function 286 30 Jul 91 Stig Andur Pedersen new email address 287 30 Jul 91 Josh Guttman Select operator (practical perspective) 288 30 Jul 91 Mike Gordon Select operator (practical perspective) 289 30 Jul 91 Rob Arthan Choice 290 02 Aug 91 Rob Arthan Yet more on the choice function 291 12 Aug 91 Garrel Pottinger Alphabetic change of bound variables 292 13 Aug 91 Kim Dam Petersen Re: Alphabetic change of bound variables 293 14 Aug 91 Ian Sutherland Re: Choice 294 15 Aug 91 Josh Guttman Re: Choice 295 15 Aug 91 Josh Guttman Choice 296 16 Aug 91 Tom Schubert user interface changes to HOL 297 19 Aug 91 David Shepherd user interface changes to HOL 298 19 Aug 91 Catia Angelo Call for turists 299 20 Aug 91 Bill Harrison Davis Night Life 300 20 Aug 91 Wim Ploegaerts Re: Davis Night Life 301 21 Aug 91 Meshell Robinson HOL91 Hotel Arrangements 302 21 Aug 91 Tom Melham Re: Alphabetic change of bound variables 303 01 Sep 91 Jeffrey Joyce UBC HOL Course Notes 304 05 Sep 91 Re: UBC HOL Course Notes 305 09 Sep 91 George Fink PM: Proof Manager 306 10 Sep 91 Tom Melham Re: UBC HOL Course Notes 307 11 Sep 91 Jeffrey Joyce NSERC Postdoctoral Fellowships 308 11 Sep 91 Roger Jones mail corruption 309 12 Sep 91 Paul Loewenstein E-mail problems 310 17 Sep 91 Konrad Slind 311 17 Sep 91 Kuang-Chien Chen mailing list for HOL 312 19 Sep 91 Please put me on the info-hol mailing list. 313 20 Sep 91 Nancy Day e-mail list 314 01 Oct 91 Konrad Slind new way to get hol90 315 03 Oct 91 Wim Ploegaerts library auxiliary, 3rd trial 316 07 Oct 91 John Van-Tassel HOL Version 2.0 317 07 Oct 91 John Van-Tassel HOL 2 318 07 Oct 91 Phil Windley HOL 2.0 available now 319 08 Oct 91 Sally Goodall CADE-11 320 08 Oct 91 John Harrison Obtaining HOL on tape & general queries 321 10 Oct 91 Kim Dam Petersen HOL90 -- for anden gang 322 10 Oct 91 Albert Camilleri Temporary Vacancy at HP Labs, Bristol 323 14 Oct 91 Phil Windley Building HOl with AKCL 324 15 Oct 91 Konrad Slind 325 15 Oct 91 Tom Melham bug in HOL version 2. 326 15 Oct 91 Phil Windley mailing list information 327 17 Oct 91 Paul Curzon bug in HOL version 2. 328 23 Oct 91 Phil Windley Isabelle 329 25 Oct 91 Adam Weitzman The "save" function 330 31 Oct 91 Tom Melham autoloading and compilation (HOL88). 331 31 Oct 91 Garrel Pottinger Referring to assumptions by number 332 31 Oct 91 Wim Ploegaerts Re: Referring to assumptions by number 333 31 Oct 91 Garrel Pottinger Re: Referring to assumptions by number 334 31 Oct 91 John Harrison Selecting assumptions 335 31 Oct 91 Wim Ploegaerts referring to assumptions cont'ed 336 31 Oct 91 Jeffrey Joyce Robin Milner - 1991 Turing Award Winner 337 31 Oct 91 Phil Windley EUARTSD Workshop Announcement; please redistribute as appropriate 338 31 Oct 91 Phil Windley Re: referring to assumptions cont'ed 339 01 Nov 91 Kim Dam Petersen X_POP_ASSUM 340 01 Nov 91 Tom Melham Re: referring to assumptions cont'ed 341 01 Nov 91 Graham Birtwistle 342 01 Nov 91 Roger Jones assumptions and proof style 343 01 Nov 91 Jim Alves-Foss 344 01 Nov 91 Garrel Pottinger Gee whiz, folks! 345 02 Nov 91 Richard Boulton Printing assumptions containing type info 346 04 Nov 91 Paul Curzon Re: referring to assumptions cont. 347 06 Nov 91 Allan Heff xholhelp alternatives 348 06 Nov 91 Phil Windley witnesses 349 06 Nov 91 Jim Alves-Foss Re: witnesses 350 07 Nov 91 John Harrison Re: witnesses 351 07 Nov 91 Tom Melham Re: witnesses 352 07 Nov 91 Phil Windley Re: witnesses 353 07 Nov 91 Paul Loewenstein witnesses 354 07 Nov 91 Jeffrey Joyce a question about define_type 355 08 Nov 91 Tom Melham Re: a question about define_type 356 08 Nov 91 Tom Melham Re: witnesses 357 09 Nov 91 Tom Melham recursive data types. 358 11 Nov 91 Tom Melham finite (*)group. 359 11 Nov 91 Rob Arthan Witnesses for a polymorphic class of groups. 360 11 Nov 91 George Fink HOL constructors 361 12 Nov 91 Zdzislaw Meglicki Which HOL? 362 13 Nov 91 John Van-Tassel AKCL + HOL version 2.0 363 14 Nov 91 Rob Arthan Witnesses for a polymorphic class of groups 364 20 Nov 91 Garrel Pottinger Completeness for the HOL logic 365 27 Nov 91 Wim Ploegaerts favour 366 27 Nov 91 Tom Melham local and multi-segment libraries. 367 29 Nov 91 Tom Melham bug in version 2.0 REFERENCE manual. 368 29 Nov 91 John Van-Tassel Anon FTP from Cambridge 369 29 Nov 91 Jeffrey Joyce forwarded message (job opportunity) 370 02 Dec 91 Brian Graham HOL versions: a measure 371 03 Dec 91 Luc Claesen Please distribute Call for Papers ICCD-92 372 04 Dec 91 Sally Goodall CADE-11: Call For Nominations 373 13 Dec 91 Simon Foley Position: Chair in Software Engineering. 374 01 Jan 92 Ching-Tsun Chou HOL on NeXT 375 03 Jan 92 Ching-Tsun Chou HELP! Trouble in running HOL on NeXT using AKCL-1-599 376 03 Jan 92 John Van-Tassel Re: HELP! Trouble in running HOL on NeXT using AKCL-1-599 377 04 Jan 92 Ching-Tsun Chou A trick that solves my problem 378 05 Jan 92 Sten Agerholm Re: HELP! Trouble in running HOL on NeXT using AKCL-1-599 379 07 Jan 92 Ray Toal 380 07 Jan 92 Richard Boulton 381 07 Jan 92 David Shepherd Re: your mail 382 09 Jan 92 Konrad Slind new hol90! 383 09 Jan 92 Hemendra Talesara Is there any HOL Users University/Researchers compiled list 384 10 Jan 92 Juanito Camilleri HOL on Solbourne S4000 385 11 Jan 92 Tom Melham Re: Is there any HOL Users University/Researchers compiled list 386 11 Jan 92 Tom Melham unwinding. 387 12 Jan 92 Chet Murthy Bound Variables 388 12 Jan 92 Mike Gordon Bound Variables 389 12 Jan 92 Hemendra Talesara RE: Is there any HOL Users University/Researchers compiled list 390 14 Jan 92 Peter Homeier HOL mailing list 391 15 Jan 92 Ching-Tsun Chou Why sets? 392 15 Jan 92 David Shepherd Re: Why sets? 393 15 Jan 92 Tom Melham Re: Why sets? 394 15 Jan 92 Roger Fleming Re: Why sets? 395 16 Jan 92 Phil Windley "What's out there?" questions 396 17 Jan 92 Wim Ploegaerts hol-emacs 397 17 Jan 92 Wim Ploegaerts "What's out there?" questions 398 17 Jan 92 Tom Melham Re: Why sets? 399 17 Jan 92 Richard Boulton Re: "What's out there?" questions 400 17 Jan 92 Mark Aagaard verification of pipelines #2 401 17 Jan 92 Mark Aagaard verification of pipelines 402 20 Jan 92 Ramu Iyer Query about testing 403 20 Jan 92 Juanito Camilleri Re: Query about testing 404 21 Jan 92 Mandayam Srivas re: verification of pipelines 405 21 Jan 92 Ashish Karkare Installing HOL. 406 21 Jan 92 Tim Leonard RE: Installing HOL. 407 22 Jan 92 Roger Jones EMACS 408 22 Jan 92 Tom Melham Re: Installing HOL. 409 22 Jan 92 Ching-Tsun Chou AKCL-1-599 -> AKCL-1-605 410 23 Jan 92 John Van-Tassel Re: AKCL-1-599 -> AKCL-1-605 411 23 Jan 92 Tom Melham Re: Installing HOL. 412 23 Jan 92 Tom Melham Re: Query about testing 413 23 Jan 92 Tom Melham Re: AKCL-1-599 -> AKCL-1-605 414 23 Jan 92 Tom Melham the sets and pred_sets libraries. 415 24 Jan 92 Tom Melham building HOL using Ibuki. 416 24 Jan 92 Tim Leonard Re: referring to assumptions cont'ed 417 26 Jan 92 Ching-Tsun Chou Overloading of constant names 418 27 Jan 92 John Harrison Re: Overloading of constant names 419 27 Jan 92 Tobias Nipkow Overloading of constant names 420 27 Jan 92 Kim Dam Petersen Re: Generic graphs (was: Overloading of constant names) 421 28 Jan 92 Garrel Pottinger Report on HOL completeness theorem 422 28 Jan 92 Garrel Pottinger Report on completeness to follow 423 29 Jan 92 Juanito Camilleri Change of address...... 424 30 Jan 92 Roger Jones EMACS thanks 425 30 Jan 92 Ching-Tsun Chou Problem with running HOL on a NeXT using AKCL-1-605 426 30 Jan 92 John Van-Tassel Re: Problem with running HOL on a NeXT using AKCL-1-605 427 31 Jan 92 Albert Camilleri Re: Query about testing 428 04 Feb 92 Tom Melham Technical Report available. 429 06 Feb 92 Ching-Tsun Chou Elsa Gunter's address 430 06 Feb 92 David Guaspari Interpolation theorem 431 07 Feb 92 David Guaspari Interpolation theorem (again) 432 08 Feb 92 Ching-Tsun Chou Restricted quantification 433 09 Feb 92 Tom Melham revisions to pred_sets library are finished. 434 10 Feb 92 Mike Gordon Need HOL Documentation? 435 10 Feb 92 Paul Loewenstein Restricted quantification 436 13 Feb 92 Luc Claesen |- HOL-92 workshop 437 13 Feb 92 Luc Claesen HOL-93 * HOL-93 * HOL-93 * HOL-93 * HOL-93 * HOL-93 * HOL-93 * HOL-93 438 13 Feb 92 Steve Brackin Huge expressions 439 13 Feb 92 Tom Melham Re: Huge expressions 440 13 Feb 92 John Harrison Re: Huge expressions 441 14 Feb 92 Brian Graham Re: Huge expressions 442 14 Feb 92 Andy Gordon Re: Restricted quantification 443 15 Feb 92 Tom Melham sets (again). 444 19 Feb 92 Steve Brackin Sorting utility 445 20 Feb 92 Tom Melham Re: Sorting utility 446 21 Feb 92 Mike Gordon HOL book 447 24 Feb 92 Doaitse Swierstra HOL book 448 24 Feb 92 Phil Windley faculty position 449 24 Feb 92 John Harrison HOL on low density tape 450 24 Feb 92 Ching-Tsun Chou Parsing paired abstraction 451 26 Feb 92 David Agnew CHDL'93 call for papers 452 26 Feb 92 Jeffrey Joyce HOL-93 workshop 453 27 Feb 92 Tom Melham Announcement --- TPCD conference 1992. 454 27 Feb 92 Juanito Camilleri 455 27 Feb 92 Ching-Tsun Chou Strange behavior of quotation parser & a question 456 28 Feb 92 John Van-Tassel Quotation parser 457 28 Feb 92 John Van-Tassel Re: Strange behavior of quotation parser & a question 458 28 Feb 92 Victor Carreno Re: Strange behavior of quotation parser & a question 459 28 Feb 92 Steve Brackin Partial instantiation 460 28 Feb 92 Inder Dhingra HOL on VMS? 461 28 Feb 92 Phil Windley Re: Partial instantiation 462 28 Feb 92 Tom Melham Re: Partial instantiation 463 29 Feb 92 K Prasad HOL, Boyer-Moore or Stateharts 464 02 Mar 92 Victor Carreno Re: HOL, Boyer-Moore or Stateharts 465 05 Mar 92 John Van-Tassel VHDL Formalisation 466 06 Mar 92 Phil Windley Proposal to Host HOL 93 467 09 Mar 92 Luc Claesen CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES 468 09 Mar 92 Doug Hoover rewriting in HOL 469 09 Mar 92 Tom Melham Re: rewriting in HOL 470 09 Mar 92 Phil Windley Re: CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES 471 09 Mar 92 Steve Brackin "Succeeds" predicate? 472 09 Mar 92 Jim Grundy Re: CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES - CALL FOR VOTES 473 09 Mar 92 Tom Melham Re: "Succeeds" predicate? 474 09 Mar 92 John Harrison Re: rewriting in HOL 475 09 Mar 92 Ching-Tsun Chou Theorem continuation functions 476 10 Mar 92 John Harrison Re: "Succeeds" predicate? 477 10 Mar 92 Mark van de Voort Re: Theorem continuation functions 478 12 Mar 92 Albert Camilleri Re: CALL FOR VOTES - CALL FOR VOTES 479 12 Mar 92 Jeffrey Joyce CALL FOR VOTES - HUG-93 480 12 Mar 92 Phil Windley Re: CALL FOR VOTES - HUG-93 481 13 Mar 92 Malcolm Newey Re: CALL FOR VOTES 482 13 Mar 92 John Carroll HOL2.0 port to PC-compatibles 483 13 Mar 92 Jim Grundy Re: CALL FOR VOTES - HUG-93 484 14 Mar 92 Luc Claesen voting on next meetings... 485 14 Mar 92 Ching-Tsun Chou Non-top-level read-eval-print loop? 486 14 Mar 92 Juanito Camilleri 487 16 Mar 92 Phil Windley Re: voting on next meetings... 488 16 Mar 92 Ramayya Kumar Withdrawl of Karlsruhe from hosting HUG-93 489 18 Mar 92 Mike Gordon Embedding HDLs in HOL 490 18 Mar 92 Michael Healy Problem 491 19 Mar 92 David Shepherd Ruby in HOL 492 19 Mar 92 Tom Melham Re: Ruby in HOL 493 19 Mar 92 Ching-Tsun Chou On using theorem continuation functions 494 20 Mar 92 Ramayya Kumar Hosing HUGs 495 25 Mar 92 Konrad Slind plea for support letters 496 26 Mar 92 Phil Windley CDA Resort 497 28 Mar 92 Ching-Tsun Chou [] problem 498 29 Mar 92 John Harrison Re: [] problem 499 30 Mar 92 Konrad Slind thanks and chnage of address 500 01 Apr 92 Jeffrey Joyce post-doc positions at UBC 501 01 Apr 92 Adam Weitzman Theorem conjuncts 502 01 Apr 92 Gavan Tredoux HOL Mailing List 503 02 Apr 92 Luc Claesen HUG-93 results of the votes. 504 02 Apr 92 Steve Brackin LIBRARIES source 505 02 Apr 92 Steve Brackin LIBRARIES source? 506 02 Apr 92 Tom Melham Re: LIBRARIES source? 507 02 Apr 92 John Harrison Re: Theorem conjuncts 508 02 Apr 92 Wilfred Chen Suggestion: A Q/A WAIS server 509 03 Apr 92 Hemendra Talesara FWD: Hardware Verification course, July 6 - 10 510 06 Apr 92 I C L Hol ICL Proof Tool Newsletter 511 06 Apr 92 Mark Aagaard interfacing thm provers and other circuit "verifiers" 512 07 Apr 92 Ramayya Kumar Re: interfacing thm provers and other circuit "verifiers" 513 08 Apr 92 Neil Murray CADE-11 514 09 Apr 92 Phil Windley [cdk@dit.upm.es (Carlos Delgado Kloos): IFIP 92] 515 09 Apr 92 Paul Loewenstein Summer position in Formal Verification 516 10 Apr 92 Matt Kaufmann connecting HOL with the Boyer-Moore Theorem Prover 517 12 Apr 92 Neil Murray CADE-11 518 13 Apr 92 John Van-Tassel DECStations and AKCL 519 13 Apr 92 Tim Leonard A wordn library. 520 13 Apr 92 John Harrison Re: A wordn library. 521 13 Apr 92 Tim Leonard Re: A wordn library. 522 13 Apr 92 Neil Murray CADE-11/more-info 523 13 Apr 92 Konrad Slind 524 14 Apr 92 Tom Melham Re: A wordn library. 525 15 Apr 92 Jeffrey Joyce 526 15 Apr 92 I C L Hol formal treatment of PLCs 527 15 Apr 92 Tom Melham 528 15 Apr 92 Jon Jacky Re: formal treatment of PLCs 529 15 Apr 92 Rob Arthan Arithmetic Challenge 530 15 Apr 92 Jeffrey Joyce arithmetic challenge 531 21 Apr 92 Neil Murray CADE-11 532 21 Apr 92 Steve Brackin Commercial SML/NJ 533 21 Apr 92 Jeffrey Joyce arithmetic challenge 534 22 Apr 92 Phil Windley mutual recursion 535 22 Apr 92 Sentot Kromodimoeljo Solution to Jeff's challenge in Eves 536 23 Apr 92 Brian Graham Re: mutual recursion 537 23 Apr 92 Tom Melham Re: mutual recursion 538 24 Apr 92 John Harrison Re: arithmetic challenge 539 24 Apr 92 Mike Fourman Commercial SML 540 26 Apr 92 Tom Melham Re: mutual recursion 541 26 Apr 92 Doug Hoover Abstract theories, subtypes, and restricted quantification 542 28 Apr 92 Sreeranga Rajan Well-founded induction? 543 28 Apr 92 Jim Grundy HOL91 Proceedings? 544 28 Apr 92 Phil Windley Re: HOL91 Proceedings? 545 28 Apr 92 Tom Melham Re: Well-founded induction? 546 28 Apr 92 Phil Windley the joyce lemma: comparing PVS and HOL (with proposals ;-) 547 29 Apr 92 Tobias Nipkow Well-founded recursion? 548 29 Apr 92 Mike Gordon Historical note on conditional rewriting 549 29 Apr 92 Mark van de Voort Re: Well-founded induction 550 29 Apr 92 Mike Fourman LAMBDA USERS MEETING 551 29 Apr 92 Ching-Tsun Chou HOL'92 paper submission deadline? 552 29 Apr 92 Kelly Hall Problems with inject_input and ML_eval in 2.0b? 553 29 Apr 92 John Harrison Re: Problems with inject_input and ML_eval in 2.0b? 554 30 Apr 92 Luc Claesen |- HOL92 announcement and call for contributions. 555 01 May 92 Tom Melham Re: Problems with inject_input and ML_eval in 2.0b? 556 04 May 92 Gavan Tredoux HOL 91 Proceedings - Request 557 04 May 92 Gavan Tredoux HOL Bibliography Database 558 04 May 92 Jim Alves-Foss Re: HOL 91 Proceedings - Request 559 04 May 92 Jim Grundy Re: HOL 91 Proceedings - Request 560 04 May 92 Jim Grundy Re: HOL Bibliography Database 561 04 May 92 Phil Windley Re: HOL Bibliography Database 562 07 May 92 Jeffrey Joyce HUG '93 563 07 May 92 Mark van de Voort discarding theory segments 564 07 May 92 Tim Leonard re: discarding theory segments 565 07 May 92 Jim Alves-Foss Labeling assumptions in the asl 566 07 May 92 Roger Jones "discarding theory segments" in ICL HOL 567 07 May 92 Tom Melham Re: Labeling assumptions in the asl 568 10 May 92 Sara Kalvala Re: Labeling assumptions in the asl 569 11 May 92 Wai Wong Re: Labeling assumptions in the asl 570 11 May 92 Wai Wong Wordn library 571 12 May 92 Tim Leonard Formal verification at Digital 572 13 May 92 Ray Toal Ackermann's function 573 14 May 92 Tom Melham Re: Ackermann's function 574 14 May 92 Andy Gordon Re: Ackermann's function 575 14 May 92 Herbert Sander Re: Ackermann's function 576 14 May 92 Tom Melham Final Call for Registration : TPCD. 577 15 May 92 Sreeranga Rajan Re: Ackermann's function 578 15 May 92 Tom Melham Recursive Functions in HOL 579 15 May 92 Roger Jones definability of functions in HOL 580 28 May 92 Jeffrey Joyce HOL on a NeXT 581 29 May 92 Kelly Hall Tamarack 3 ML files? 582 30 May 92 Tom Melham Re: Tamarack 3 ML files? 583 30 May 92 Tom Melham mistake. 584 01 Jun 92 Ching-Tsun Chou CASES_THENL and DISJ_CASES_THENL 585 02 Jun 92 Ramayya Kumar Public domain version of the prover FAUST 586 03 Jun 92 Ramayya Kumar FAUST also at HOL-FTP site 587 07 Jun 92 Neil Murray CADE-11 588 09 Jun 92 Donald Syme HOL: Struggling with mutually recursive types 589 09 Jun 92 Phil Windley Abstract Theories in HOL 590 09 Jun 92 Tom Melham Re: HOL: Struggling with mutually recursive types 591 10 Jun 92 Phil Windley abstract theory package location 592 10 Jun 92 Ching-Tsun Chou UNDIRECTED graph theory in HOL? 593 11 Jun 92 Inder Dhingra New Addition 594 11 Jun 92 Luc Claesen Reminder: Paper contributions for |- HOL-92 ! 595 11 Jun 92 Luc Claesen Email submissions for |- HOL92 (info) 596 11 Jun 92 Wai Wong Re: UNDIRECTED graph theory in HOL? 597 12 Jun 92 Building HOL with Allegro 4.1 598 12 Jun 92 John Van Tassel Re: Building HOL with Allegor 4.1 599 15 Jun 92 Phil Windley [Wishnu Prasetya: bad varstruct??] 600 15 Jun 92 Tom Melham Re: [Wishnu Prasetya: bad varstruct??] 601 16 Jun 92 Donald Syme HOL88 ML Syntax Checkers 602 16 Jun 92 David Shepherd Re: [Wishnu Prasetya: bad varstruct??] 603 16 Jun 92 David Shepherd Re: [Wishnu Prasetya: bad varstruct??] 604 16 Jun 92 Wishnu Prasetya ISPEC definition 605 16 Jun 92 John Harrison Re: [Wishnu Prasetya: bad varstruct??] 606 16 Jun 92 John Harrison Re: ISPEC definition 607 17 Jun 92 Tom Melham Re: inputs to new_recursive_definition 608 17 Jun 92 John Harrison Libraries for Version 2.1 609 18 Jun 92 Wishnu Prasetya Failure to load Abstract Theory 610 18 Jun 92 Mike Gordon Can anyone help? 611 18 Jun 92 Steve Brackin HOL88 directory structure 612 18 Jun 92 Ching-Tsun Chou Temporal logic in HOL 613 24 Jun 92 Tom Schubert HOL port to Caml? 614 25 Jun 92 Phil Weiss Looking for someone with experience translating Z to HOL 615 26 Jun 92 David Shepherd Re: Looking for someone with experience translating Z to HOL 616 26 Jun 92 Phil Weiss Nevermind 617 29 Jun 92 Kim Dam Petersen COND_RES_TAC ? 618 6 Jul 92 Mark van de Voort building HOL on SUN4/AKCL 619 6 Jul 92 John Van Tassel Re: building HOL on SUN4/AKCL 620 7 Jul 92 Sreeranga Rajan constant name reuse 621 7 Jul 92 Phil Windley Re: constant name reuse 622 7 Jul 92 Ching-Tsun Chou Re: constant name reuse 623 8 Jul 92 Konrad Slind Re: constant name reuse 624 8 Jul 92 Tobias Nipkow Overloading 625 8 Jul 92 John Harrison Re: constant name reuse 626 8 Jul 92 Wishnu Prasetya problem with long string? 627 8 Jul 92 Ching-Tsun Chou What is $# in the HOL logic? 628 8 Jul 92 Tom Melham Re: What is $# in the HOL logic? 629 9 Jul 92 Ching-Tsun Chou Re: What is $# in the HOL logic? 630 9 Jul 92 Ching-Tsun Chou Binders 631 13 Jul 92 Kelly Hall HOL on HP 730? 632 15 Jul 92 Ching-Tsun Chou Sum over set 633 15 Jul 92 Ching-Tsun Chou Recursive definition over sets 634 15 Jul 92 David Outteridge Formal methods position. 635 15 Jul 92 Phil Weiss Re: Recursive definition over sets 636 15 Jul 92 David Shepherd Re: Recursive definition over sets 637 15 Jul 92 Phil Weiss Re: Recursive definition over sets 638 15 Jul 92 John Harrison Re: Recursive definition over sets 639 16 Jul 92 Albert Camilleri Re: HOL on HP 730? 640 16 Jul 92 Wishnu Prasetya State Logic 641 17 Jul 92 Phil Weiss More help on recursion over sets 642 17 Jul 92 Phil Weiss Figured it out (set recursion) 643 18 Jul 92 Ching-Tsun Chou Generalizing an assoc. and comm. operation with id. to sets 644 23 Jul 92 Wishnu Prasetya unbounded type in definition 645 23 Jul 92 David Shepherd Re: unbounded type in definition 646 23 Jul 92 Phil Weiss Equivalence of GSPEC(\x. ( ,F)) and EMPTY 647 24 Jul 92 Wai Wong Restricted quantifiers 648 24 Jul 92 David Shepherd Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY 649 24 Jul 92 Tom Melham Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY 650 24 Jul 92 Tom Melham Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY 651 24 Jul 92 John Harrison Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY 652 24 Jul 92 Wishnu Prasetya How to prove this shortly? 653 24 Jul 92 Wai Wong Re: How to prove this shortly? 654 24 Jul 92 Victor Carreno Re: How to prove this shortly? 655 24 Jul 92 Phil Weiss More on GSPEC(\x.(,F)) 656 27 Jul 92 Tom Melham Re: How to prove this shortly? 657 27 Jul 92 John Harrison Re: How to prove this shortly? 658 27 Jul 92 Lawrence Paulson Re: How to prove this shortly? 659 27 Jul 92 Phil Weiss Set parsing? 660 27 Jul 92 Jobs 661 27 Jul 92 Jim Alves-Foss Re: Set parsing? 662 28 Jul 92 Tom Melham Re: Set parsing? 663 28 Jul 92 Kelly Hall Problems with AKCL HOL HP9000/700 664 28 Jul 92 Gavan Tredoux CHOOSE breaks 665 29 Jul 92 Tom Melham Re: CHOOSE breaks 666 30 Jul 92 Roger Jones stripping failure 667 31 Jul 92 Victor Carreno Re: stripping failure 668 01 Aug 92 John Harrison Re: CHOOSE breaks 669 02 Aug 92 Tom Melham Re: stripping failure 670 03 Aug 92 Victor Carreno the case of the lost postings