Appeared in Volume 7/1, February 1994
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:
Unfortunately, Isabelle-93 is not upwards compatible with its predecessor. See Doc/CHANGES-93.txt for advice, particularly on converting to the new simplifier.
Isabelle-93 is available by anonymous FTP from the Univ. of Cambridge:
Isabelle-93 is also available from the Technical Univ. of Munich. Connect
The file Isabelle93.tar.gz should be gunzipped, then extracted using tar:
gunzip -c Isabelle93.tar.gz | tar xf -
For more information contact:
Lawrence C Paulson Computer Lab., Univ. of Cambridge Cambridge CB2 3QG, UK Email: Larry.Paulson@cl.cam.ac.uk Tel: +44 223 334 600 Fax: +44 223 334 678 Tobias Nipkow Institut für Informatik, TU München 80290 München, Germany Email: Tobias.Nipkow@informatik.tu-muenchen.de Tel: +49 89 21 052 690 Fax: +49 89 21 058 183