The theorem-prover Isabelle

Date: Wed, 17 Jan 90 11:45:34 GMT
To: 	proof%cs.chalmers.se@nsfnet-relay.ac.uk,


Isabelle is a generic theorem prover. It suppports interactive proof in
several formal systems, including first-order logic (intuitionistic and
classical), higher-order logic, Martin-L\"of type theory, and
Zermelo-Fraenkel set theory. New logics can be introduced by specifying
their syntax and rules of inference. Both natural deduction and sequent
calculi are allowed. Isabelle is written in Standard ML.

This release includes an Earley-type parser generator. Syntax rules are
specified in a mixfix notation, with pretty printing annotations. Some
translations still have to be coded in ML (particularly those involving
variable binding), but the rest is automatic.

The Manual has been completely rewritten. Its 150 pages include a gentle
introduction to Isabelle, descriptions of the built-in logics, and
discussion of advanced techniques. Every section contains several sample

To existing license holders. You may obtain this release by e-mail, if
possible. Isabelle's new syntax, while far more concise, is not upwards
compatible with previous releases. Tools are provided to help you convert
to the new syntax.

For more information, please contact

Tobias Nipkow 		  		E-mail: tnn@cl.cam.ac.uk 
Computer Laboratory 			Phone: +44-223-334600
University of Cambridge 		Fax: +44-223-334748 
Pembroke Street 
Cambridge CB2 3QG 

or (until July 1990; thereafter at Cambridge)

Lawrence C Paulson			E-mail: lcp@lfcs.ed.ac.uk
Department of Computer Science		Phone: +44-31-667-1081
University of Edinburgh
Mayfield Road
Edinburgh EH9 3JZ