Subject: new mirror sites!
From: Lawrence C Paulson <[email-masked]>
To: [email-masked]
Date: Wed, 18 Feb 1998 17:38:56 +0000

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 [email-masked]
Conference announcements should be relevant and brief

To: [email-masked], [email-masked]
Subject: Announcing Isabelle 98
Organization: Computer Laboratory, University of Cambridge, England
Date: Thu, 15 Jan 1998 12:28:39 +0000
From: Lawrence C Paulson <[email-masked]>

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: [email-masked]
Subject: new Isabelle logo!
Organization: Computer Laboratory, University of Cambridge, England
Date: Mon, 06 Oct 1997 12:17:28 +0100
From: Lawrence C Paulson <[email-masked]>
Sender: Larry Paulson <[email-masked]>

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

<A HREF="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"> <IMG
SRC="Isabelle.gif" ALIGN=RIGHT ALT="Isabelle logo"></A>

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 [email-masked]
Conference announcements should be relevant and brief

X-Mailer: exmh version 1.6.4+cl+patch 10/10/95
To: [email-masked]
Subject: Isabelle update
X-Uri: <URL:http://www.cl.cam.ac.uk/users/lcp>
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 <[email-masked]>
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: [email-masked] (Tony Cant)
To: [email-masked]
Subject: XIsabelle-2.0
Cc: [email-masked], [email-masked]

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: [email-masked], [email-masked])

==============================================================================
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 <[email-masked]> Wed, 4 Oct 
                   1995 17:50:00 +0100
Pp-Warning: Illegal Received field on preceding line
From: Burkhart Wolff <[email-masked]>
Date: Wed, 4 Oct 1995 17:46:54 +0100
To: [email-masked]
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: [email-masked]
Subject: Isabelle update
X-Uri: <URL:http://www.cl.cam.ac.uk/users/lcp>
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 <[email-masked]>

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: [email-masked]
Subject: Position papers required
X-Uri: <URL:http://www.cl.cam.ac.uk/users/lcp>
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 <[email-masked]>

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 [email-masked] or
by post to 
	Lawrence C Paulson, Computer Laboratory, University of Cambridge,
	Pembroke Street, Cambridge CB2 3QG, England

Deadline: Friday 2nd June 1995

==============================================================================
To: [email-masked]
Subject: Isabelle94 release 3
Date: Wed, 26 Apr 1995 15:43:15 +0100
From: Lawrence C Paulson <[email-masked]>

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 <a,b>.  

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: [email-masked]
Subject: Isabelle update
Date: Fri, 20 Jan 1995 16:41:12 +0000
From: Lawrence C Paulson <[email-masked]>

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: [email-masked]
Subject: Another User Interface
Date: Mon, 26 Sep 94 12:05:25 +0100
From: Lawrence C Paulson <[email-masked]>

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
[email-masked].

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: [email-masked], [email-masked])

==============================================================================
To: [email-masked], [email-masked],
        [email-masked], [email-masked],
        [email-masked]
Subject: ISABELLE-94
Date: Fri, 16 Sep 94 09:58:07 +0100
From: Lawrence C Paulson <[email-masked]>

			    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
[email-masked]	    [email-masked]
==============================================================================
To: [email-masked], [email-masked],
        [email-masked], [email-masked],
        [email-masked]
Subject: ISABELLE BOOK NOW AVAILABLE
Date: Fri, 16 Sep 94 10:00:12 +0100
From: Lawrence C Paulson <[email-masked]>

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:[email-masked]>
To: [email-masked], [email-masked], [email-masked],
        [email-masked], [email-masked],
        [email-masked], [email-masked]
Subject: new Isabelle available by ftp
Date: Thu, 16 Dec 93 14:36:02 +0000
From: Lawrence C Paulson <[email-masked]>

		       		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: <your internet address>
   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: [email-masked] 
Computer Laboratory 		Phone: +44-223-334600
University of Cambridge 	Fax:   +44-223-334678
Pembroke Street 
Cambridge CB2 3QG 
England

Tobias Nipkow 		  	E-mail: [email-masked]
Institut f\"ur Informatik	Phone: +49-89-21052690
TU M\"unchen			Fax:   +49-89-21058183
80290 M\"unchen
Germany