To: isabelle-users@cl.cam.ac.uk Subject: new mirror sites! Date: Wed, 18 Feb 1998 17:38:56 +0000 From: Lawrence C Paulson Isabelle is now also distributed from Bell Labs, New Jersey: ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html Also, Standard ML of New Jersey (Version 110.0.3) is now distributed from Cambridge: ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/ -- Larry Paulson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief To: isabelle-users@cl.cam.ac.uk, theorem-provers@mc.lcs.mit.edu Subject: Announcing Isabelle 98 Organization: Computer Laboratory, University of Cambridge, England Date: Thu, 15 Jan 1998 12:28:39 +0000 From: Lawrence C Paulson Isabelle98 is now available. Here are some highlights: * hierachically structured name spaces: no more name conflicts involving constants, axioms, etc. declared in different theories * a graphical theory browser (in Java) * extensible records for HOL (still experimental) * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions * HOL/Auth: new security protocol proofs, including some for the Internet protocol TLS There are many internal improvements, too. Isabelle98 is available from Cambridge http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ and from Munich http://www4.informatik.tu-muenchen.de/~isabelle/dist/ An unofficial binary distribution of SML/NJ 110 for Linux/x86 is available at http://www4.informatik.tu-muenchen.de/~isabelle/smlnj-110/ Thanks again to Markus Wenzel, Tobias Nipkow and their colleagues at TUM for very substantial contributions. -- Larry Paulson To: isabelle-users@cl.cam.ac.uk Subject: new Isabelle logo! Organization: Computer Laboratory, University of Cambridge, England Date: Mon, 06 Oct 1997 12:17:28 +0100 From: Lawrence C Paulson Sender: Larry Paulson We now have a winner! Logo number 8, by Franziska Wenzel, was the favourite throughout the voting and most of the time had an overall majority. By this morning, there were enough votes for other entries (including Chris Owen's late number 9) to require three rounds of counting. Details are on the Web page. I'm not certain I implemented STV perfectly, but number 8 was clearly the overwhelming choice. (Incidentally, it was designed on an Apple Mac.) There were a couple of late ballots, but they would not have changed the outcome. The new logo has now replaced my old one (number 1) on http://www.cl.cam.ac.uk/Research/HVG/Isabelle/, etc. Your Isabelle-related pages could link to the Isabelle home page by something like Isabelle logo Before getting a local copy of Isabelle.gif, you might want to wait a few days in case the author tries some fine-tuning. Many, many thanks to everybody who contributed logos, many of which were delightful, and also to everybody who voted. -- Larry Paulson -------- Send messages to isabelle-users@cl.cam.ac.uk Conference announcements should be relevant and brief X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 To: isabelle-users@cl.cam.ac.uk Subject: Isabelle update X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Mon, 22 Jan 1996 09:51:16 +0100 From: Lawrence C Paulson Content-Type: text Content-Length: 849 A new update of Isabelle, Isabelle94-5, is now on the Cambridge ftp site. The URL is ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-5.tar.gz It is also on the Munich site, at URL ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/Isabelle94-5.tar.g z Here is a summary of changes from Isabelle94-4. Space requirements are reduced again, by about forty percent! Theories can be automatically converted to HTML for publishing on the World Wide Web and for browsing using Netscape or Mosaic. Point your browser at index.html. For details see section 6.5, "Generating HTML documents" in the Reference Manual. Theory files no longer require "..." (quotes) around most types. There are new examples, including two proofs of the Church-Rosser theorem. The non-curried (1994) version of HOL is no longer distributed. -- Larry Paulson Date: Fri, 13 Oct 95 10:27:53 CST From: cant@itd.dsto.gov.au (Tony Cant) To: isabelle-users@cl.cam.ac.uk Subject: XIsabelle-2.0 Cc: cant@itd.dsto.gov.au, maris@itd.dsto.gov.au Announcement ============ A new release (2.0) of the source code for XIsabelle, a prototype Graphical User Interface for the Isabelle theorem prover developed at DSTO, is now available by anonymous ftp from the University of Cambridge. XIsabelle requires version Isabelle94-4 of Isabelle. This code is being released on the understanding that it will be used for research purposes only, and that any reference to it acknowledges DSTO. The code can be freely copied and distributed as long as any copies include this release information. XIsabelle has been designed to run with either Standard ML of New Jersey (tested for Version 0.93) or Poly/ML (tested for Version 2.06). XIsabelle is now implemented using Tcl/Tk and Expect. It uses Tcl Version 7.4 and Tk Version 4.0, available by anonymous ftp from ftp.smli.com in the directory pub/tcl. It will not work with earlier versions. XIsabelle also requires the program Expectk, built from these versions of Tcl/Tk. You will need Expect Version 5.18, available by anonymous ftp from ftp.cme.nist.gov in the directory pub/expect. XIsabelle can be obtained by Web browsers via the URL ftp://ftp.cl.cam.ac.uk/ml/XIsabelle-2.0.tar.gz Alternatively, anonymous ftp can be used: * Connect to host ftp.cl.cam.ac.uk * Use login id "anonymous" with your internet address as password * put ftp in BINARY MODE ("binary") * go to directory ml (by typing "cd ml") * "get" the file XIsabelle-2.0.tar.gz from that directory. The file XIsabelle-2.0.tar.gz should be uncompressed, using the command gunzip XIsabelle-2.0.tar.gz This will give the tar file XIsabelle-1.8.tar. The command tar xvf XIsabelle-2.0.tar will unpack this file to the directory XIsabelle-2.0. Installation instructions can be found in the README file on the distribution. XIsabelle is still under development. We would be most grateful to receive any feedback from users of XIsabelle. ================================================================= Tony Cant and Maris Ozols Trusted Computer Systems Group Information Technology Division Defence Science and Technology Organisation PO Box 1500 SALISBURY South Australia 5108 (email: tony.cant@dsto.defence.gov.au, maris.ozols@dsto.defence.gov.au) ============================================================================== Original-Received: by bettina.informatik.uni-Bremen.de (8.6.10/3.10.94m) with SMTP from spica.informatik.uni-bremen.de [134.102.204.27] id RAA09748 for Wed, 4 Oct 1995 17:50:00 +0100 Pp-Warning: Illegal Received field on preceding line From: Burkhart Wolff Date: Wed, 4 Oct 1995 17:46:54 +0100 To: isabelle-users@cl.cam.ac.uk Subject: ANNOUNCE sml_tk X-Sun-Charset: US-ASCII sml_tk is a toolkit for tcl/Tk entirely written in and for sml. It runs fine under NJML and currently slightly hampered under POLY/ML (strange internal buffer-problems of POLY with IO). It provides a means to write (small) grafical user interfaces or all sorts of demo-tools in sml. It can be expected that by using the modularity-features of sml, a much higher degree of abstraction and reuse of components can be achieved than with the relatively poor structuring mechanisms provided by tcl. sml_tk is distributed under usual PD-conditions. We intend to build future releases, but I can't tell what will be done next. I can't promise that any BUGS will be fixed or that I will even answer e-mail concerning technical questions over sml_tk. You are encouraged to modify and extend it. I will see if I can integrate larger extensions into the standard-distribution. You can get more information and the sources from my "Isabelle-Distribution-Page" http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html bu [PS: Larry - would you please integrate this www-address into your intended/prepared "Isabelle around the world"-page?] ============================================================================== X-Mailer: exmh version 1.6.1 5/23/95 To: isabelle-users@cl.cam.ac.uk Subject: Isabelle update X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Fri, 18 Aug 1995 12:16:16 +0100 From: Lawrence C Paulson A new update of Isabelle, Isabelle94-4, is now on the Cambridge ftp site. The URL is ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-4.tar.gz It is also on the Munich site, at URL ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/Isabelle94-4.tar.g z Here is a summary of changes from Isabelle94-3. Space requirements are much reduced, thanks to changes to the parser and classical reasoner. Theory files (.thy) no longer require \...\ escapes to break lines. You can search the theorem database. See the section "Retrieving theorems" on page 8 of the (updated) Reference Manual. There are new examples, especially Grabczewski's monumental case study involving the Axiom of Choice. The previous version of HOL is now called Old_HOL. It will disappear altogether in Isabelle-95! The new version of HOL (previously called CHOL) uses a curried syntax for functions. Application looks like f a b instead of f(a,b). Mutually recursive inductive definitions finally work in HOL. In ZF, pattern-matching on tuples is now available in all abstractions. It translates to the operator "split". (Previously this was only available in HOL.) Larry Paulson Tobias Nipkow ============================================================================== X-Mailer: exmh version 1.6 4/21/95 To: isabelle-users@cl.cam.ac.uk Subject: Position papers required X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Tue, 16 May 1995 09:35:03 +0100 From: Lawrence C Paulson The ESPRIT project TYPES, which funds the development of several proof systems (Alf, Coq, Isabelle and Lego), requires brief "position papers" as a deliverable. These should come from external sites (preferably industrial) and discuss an application of our proof systems. More details are attached below. If your site could write a position paper, please let me know. Larry Paulson "POSITION PAPERS" -- SUGGESTED GUIDELINES TOTAL LENGTH: one or two pages. Please say a few words about who you are and outline your main research interests. Indicate your need for formal methods, whether this has industrial relevance, etc. Please outline your experience (if any) with other systems such as Boyer-Moore, HOL, OBJ or LARCH. Please outline your experience with one or several proof systems from the Types project, describing difficulties encountered, positive results, quality of documentation, assistance from implementers to fix problems, etc. --or-- Please outline your proposed work using proof systems from the Types project. Please comment on whether our approach is headed in the right direction, what else is needed, etc. ------ Please send by email (in PostScript or dvi format) to lcp@cl.cam.ac.uk or by post to Lawrence C Paulson, Computer Laboratory, University of Cambridge, Pembroke Street, Cambridge CB2 3QG, England Deadline: Friday 2nd June 1995 ============================================================================== To: isabelle-users@cl.cam.ac.uk Subject: Isabelle94 release 3 Date: Wed, 26 Apr 1995 15:43:15 +0100 From: Lawrence C Paulson A new update of Isabelle, Isabelle94-3, is now on the Cambridge ftp site. The URL is ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-3.tar.gz It is also on the Munich site. Here is a summary of changes from Isabelle94-2. There is a new infix operator, addss, allowing the classical reasoner to perform simplification at each step of its search. Example: fast_tac (cs addss ss) This still performs depth-first search, and so differs from using setsolver to make the simplifier call the classical reasoner. There is a new logic, CHOL. It is the same as HOL, but with a curried syntax for functions. Application looks like f a b instead of f(a,b). Also pairs look like (a,b) instead of . PLEASE NOTE: CHOL will replace HOL in Isabelle-95! In CHOL, pattern-matching on tuples is now available in all abstractions. It translates to the operator "split". A new theory of integers is available. In ZF, integer numerals now denote two's-complement binary integers. Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML. There are many new examples: I/O automata, Church-Rosser theorem, equivalents of the Axiom of Choice. Thanks to everyone who provided theories or examples. Their names are acknowledged on the individual files. Larry Paulson ============================================================================== To: isabelle-users@cl.cam.ac.uk Subject: Isabelle update Date: Fri, 20 Jan 1995 16:41:12 +0000 From: Lawrence C Paulson A new update of Isabelle, Isabelle94-2, is now on the Cambridge and Munich ftp sites, URL ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-2.tar.gz Here is a summary of changes from Isabelle94-1. Resolution is significantly faster. The different sections in a .thy file can now be mixed and repeated freely. There is now a database of theorems for FOL, HOL and ZF. New commands including qed, qed_goal and bind_thm store theorems in the database. At present the database only allows simple queries: return a named theorem (get_thm) or all theorems of a given theory (thms_of), or find out what theory a theorem was proved in (theory_of_thm). The database could be useful to designers of user interfaces. Bugs have been fixed in the inductive definition and datatype packages. The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs and HOL_dup_cs obsolete. Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1 have been removed. ZF has a new definition of function space; it is equivalent but easier to use. ZF also has many new results about cardinal and ordinal arithmetic (some due to Krzysztof Grabczewski). HOL now supports a 'subtype' facility for introducing new types as subsets of existing types. We expect to release updates like this every couple of months, instead of waiting a year between releases as before. Many users will not need to pick up each update. Larry Paulson Tobias Nipkow ============================================================================== To: isabelle-users@cl.cam.ac.uk Subject: Another User Interface Date: Mon, 26 Sep 94 12:05:25 +0100 From: Lawrence C Paulson The first release (1.8) of the source code for XIsabelle, an experimental graphical user interface for Isabelle, is now available by anonymous ftp from the University of Cambridge. It comes courtesy of Tony Cant and Maris Ozols of DSTO, South Australia; their address appears below. XIsabelle is implemented using PolyML, using X and Motif functions. At this stage, it has not been implemented in Standard ML of New Jersey. To purchase Poly/ML with Motif, send email to Abstract Hardware Ltd at lambda@ahl.co.uk. How to get XIsabelle: Mosaic users, load the URL ftp://ftp.cl.cam.ac.uk:/ml/XIsabelle-1.8.tar.gz. FTP Instructions: * Connect to host ftp.cl.cam.ac.uk * Use login id "anonymous" with your internet address as password * put ftp in BINARY MODE ("binary") * go to directory ml (by typing "cd ml") * "get" the file XIsabelle-1.8.tar.gz from that directory. The file XIsabelle-1.8.tar.gz should be uncompressed, using the command gunzip XIsabelle-1.8.tar.gz This will give the tar file XIsabelle-1.8.tar. The command tar xvf XIsabelle-1.8.tar will unpack this file to the directory XIsabelle-1.8. Installation instructions can be found in the README file on the distribution. ================================================================= A Cant and M A Ozols Trusted Computer Systems Group Information Technology Division Defence Science and Technology Organisation PO Box 1500 SALISBURY South Australia 5108 (email: cant@itd.dsto.gov.au, maris@itd.dsto.gov.au) ============================================================================== To: theorem-provers@mc.lcs.mit.edu, info-hol@leopard.cs.byu.edu, logic@cs.cornell.edu, bra-types@cs.chalmers.se, isabelle-users@cl.cam.ac.uk Subject: ISABELLE-94 Date: Fri, 16 Sep 94 09:58:07 +0100 From: Lawrence C Paulson ISABELLE-94 We are please to announce a new version of Isabelle. A generic theorem prover, Isabelle supports a classical set theory, a constructive type theory, higher-order logic, modal logics, etc. Isabelle-94 is significantly faster than Isabelle-93. In its higher-order logic and set theory, you can easily make (co)inductive and datatype definitions. In higher-order logic, primitive recursive functions can now be defined directly. In set theory, you can define trees that are infinitely branching or infinitely deep. Isabelle is available by ftp from host ftp.cl.cam.ac.uk, directory ml. Consult the file isabelle.txt for more information on Isabelle and ftp instructions. For Mosaic users, the following URLs are relevant: * for information on Isabelle, open http://www.cl.cam.ac.uk/Research/HVG/isabelle.html * for an index to the Isabelle ftp area, open ftp://ftp.cl.cam.ac.uk/ml/index.html Lawrence C. Paulson Tobias Nipkow Computer Laboratory Institut f|r Informatik University of Cambridge TU M|nchen Cambridge CB2 3QG 80290 M|nchen England Germany Larry.Paulson@cl.cam.ac.uk Tobias.Nipkow@informatik.tu-muenchen.de ============================================================================== To: theorem-provers@mc.lcs.mit.edu, info-hol@leopard.cs.byu.edu, logic@cs.cornell.edu, bra-types@cs.chalmers.se, isabelle-users@cl.cam.ac.uk Subject: ISABELLE BOOK NOW AVAILABLE Date: Fri, 16 Sep 94 10:00:12 +0100 From: Lawrence C Paulson Isabelle: A Generic Theorem Prover by Lawrence C. Paulson, with contributions by Tobias Nipkow Springer Lecture Notes in Computer Science 828 Price: DM 66.00 XVII+321 pages, 1994. This book provides complete documentation of the theorem prover Isabelle. It includes an introduction, a general reference section, and documentation of the main logics provided with Isabelle. The book is closely based on the three Isabelle manuals distributed electronically with Isabelle. But it is a single volume with a global index. Mosaic users can call up a description of Isabelle via the URL http://www.cl.cam.ac.uk/Research/HVG/isabelle.html A plain text version is available by ftp from ftp.cl.cam.ac.uk, file ml/isabelle.txt. An errata list for the book is available using Mosaic or ftp: ftp://ftp.cl.cam.ac.uk/ml/ERRATA.txt Lawrence C. Paulson Computer Laboratory University of Cambridge Cambridge CB2 3QG England ============================================================================== Return-Path: <@swan.cl.cam.ac.uk:Larry.Paulson@cl.cam.ac.uk> To: logic@cs.cornell.edu, lprolog@cis.upenn.edu, types@dcs.gla.ac.uk, isabelle-users@cl.cam.ac.uk, proof-sci@cs.chalmers.se, info-hol@cs.uidaho.edu, theorem-provers@mc.lcs.mit.edu Subject: new Isabelle available by ftp Date: Thu, 16 Dec 93 14:36:02 +0000 From: Lawrence C Paulson ISABELLE-93 Isabelle is a generic theorem prover. New logics are introduced by specifying their syntax and rules of inference. Proof procedures can be expressed using tactics and tacticals. The latest version, Isabelle-93, is significantly faster than Isabelle-92 and has several other improvements. * Theories may now specify rewrite rules for syntax. This eliminates most ML code from syntax definitions, and conveniently handles trivial definitions such as 1==succ(0). Theory dependencies are now recorded internally; Isabelle can auto-load a theory's ancestors. A search path variable specifies where Isabelle should look for theory files. * For ZF only, Isabelle now provides a comprehensive inductive and coinductive definition package using least and greatest fixedpoints. Isabelle provides a high degree of automation: * A generic simplifier performs rewriting by equality relations such as = and <->. It handles conditional rewrite rules, can perform automatic case splits, and extracts rewrite rules from the context while descending into an expression. [Compatibility note: This simplifier is much faster and easier to use than Isabelle-92's. Congruence rules are no longer required! The old simplifier remains available for the time being because it is more general than the new one.] * A generic package supports classical reasoning in first-order logic, set theory, etc. Isabelle can support a wide variety of logics, and comes with several built-in ones: * many-sorted first-order logic, constructive and classical versions * higher-order logic, similar to that of Gordon's HOL * Zermelo-Fraenkel set theory * an extensional version of Martin-L\"of's Type Theory * the classical first-order sequent calculus LK * the modal logics T, S4, and S43 * the Logic for Computable Functions, LCF * the Lambda Cube Isabelle's Zermelo-Fraenkel set theory derives a theory of functions, well-founded recursion, and several recursive data structures (including mutually recursive trees and forests, as well as infinite lists). Higher-order logic has similar features. Both logics are sufficiently developed to support high-level proofs. Isabelle-93 includes extensive documentation, on the subdirectory Doc: * "Introduction to Isabelle" explains the basic concepts at length, and gives examples. (71 pages) * "The Isabelle Reference Manual" documents nearly all most of Isabelle's facilities, apart from particular object-logics. (85 pages) * "Isabelle's Object-Logics" describes the various logics supplied with Isabelle. It also describes how to define new logics. (166 pages) * "A Fixedpoint Approach to Implementing (Co)Inductive Definitions" describes the induction/coinductive definition package for ZF. (31 pages) --------------------------------------------------------------------------- Isabelle-93 is available by anonymous ftp from the University of Cambridge. Instructions: * Connect to host ftp.cl.cam.ac.uk [128.232.0.56] * Use login id "ftp" with your internet address as password * put ftp in BINARY MODE ("binary") * go to directory ml (by typing "cd ml") * "get" the file Isabelle93.tar.gz from that directory. Here is a sample dialog: ftp ftp> open ftp.cl.cam.ac.uk Name: ftp Password: ftp> binary ftp> cd ml ftp> get Isabelle93.tar.gz ftp> quit Isabelle-93 is also available from the Technical University of Munich. Connect to host ftp.informatik.tu-muenchen.de [131.159.0.198]; go to directory local/lehrstuhl/nipkow. The addresses 128.232.0.56 and 131.159.0.198 are correct as of 12/93 but are subject to change over time. The names ftp.cl.cam.ac.uk and ftp.informatik.tu-muenchen.de are permanent. --------------------------------------------------------------------------- The file Isabelle93.tar.gz should be gunzipped, then extracted using tar: gunzip -c Isabelle93.tar.gz | tar xf - [gunzip is a GNU compression utility and is available from the usual sites.] This will create the directory Isabelle93, which should contain 13 subdirectories; its total size is about 3 megabytes. The file COPYRIGHT contains the Copyright notice and Disclaimer of Warranty. The file README contains instructions for compiling Isabelle. Unfortunately, Isabelle-93 NOT upwards compatible with its predecessor. See Doc/CHANGES-93.txt for advice, particularly on converting to the new simplifier. --------------------------------------------------------------------------- Lawrence C Paulson E-mail: Larry.Paulson@cl.cam.ac.uk Computer Laboratory Phone: +44-223-334600 University of Cambridge Fax: +44-223-334678 Pembroke Street Cambridge CB2 3QG England Tobias Nipkow E-mail: Tobias.Nipkow@informatik.tu-muenchen.de Institut f\"ur Informatik Phone: +49-89-21052690 TU M\"unchen Fax: +49-89-21058183 80290 M\"unchen Germany