wenzelm@3259: wenzelm@3259: wenzelm@3259: wenzelm@3259: wenzelm@3259: wenzelm@3259: The Isabelle System Distribution wenzelm@3259: wenzelm@3259: wenzelm@3259: wenzelm@3259: wenzelm@3259:

The Isabelle System Distribution

wenzelm@3259: wenzelm@3259:

Version information

wenzelm@3259: wenzelm@11575: This is the internal repository version of Isabelle. See the wenzelm@11575: NEWS file in the distribution for details on user-relevant wenzelm@11575: changes. wenzelm@3259: wenzelm@3259: wenzelm@3259:

System requirements

wenzelm@3259: wenzelm@11575: Isabelle requires a real Unix box with sufficient resources, say 64 MB wenzelm@11575: of free main memory and a decent CPU. Speaking by today's hardware wenzelm@11575: standards, any moderate Linux box should give a very nice platform for wenzelm@11575: Isabelle. wenzelm@3259: wenzelm@3259:

wenzelm@3259: wenzelm@6077: Furthermore, Isabelle needs the following software, which is not part wenzelm@6077: of the distribution: wenzelm@3259:

wenzelm@3259: wenzelm@3259:

wenzelm@3259: wenzelm@3259: The following ML system and platform combinations are known to work wenzelm@6077: very well: wenzelm@3259:

wenzelm@3259: wenzelm@8809:

Poly/ML, previously a wenzelm@8809: commercial product, is back in the free world. It is by far the best wenzelm@8809: compiler for running Isabelle, requiring the least memory and offering wenzelm@8809: the highest performance. wenzelm@3259: paulson@8385:

SML/NJ wenzelm@8809: needs lots of store and disk space, but supports many more platforms. wenzelm@8809: The current official release is 110. Basically, we still support the wenzelm@9406: old 0.93 release, but do not recommend to use it under normal wenzelm@9406: circumstances. wenzelm@3259: wenzelm@11575:

MLWorks used to be a commercial ML programming environment wenzelm@11575: developed by Harlequin and was wenzelm@11575: unfortunately withdrawn after that company was taken over. Isabelle wenzelm@11575: on MLWorks 2.0 works reasonably well. wenzelm@3259: wenzelm@3259: wenzelm@3259:

Installation

wenzelm@3259: wenzelm@9927: Binary packages are available for Isabelle/HOL and ZF on the Linux/x86 wenzelm@8809: platform. The system may be easily built from scratch as well, taking wenzelm@9927: the traditional tar.gz source distribution. See file INSTALL wenzelm@9927: as distributed with Isabelle for more information. wenzelm@8809: wenzelm@6486: Further background information may be found in the Isabelle System wenzelm@6486: Manual, distributed with the sources (directory doc). wenzelm@3259: wenzelm@3259: wenzelm@9927:

User interface

wenzelm@6077: wenzelm@9927: The canonical Isabelle user interface is Proof General by David Aspinall wenzelm@10079: and others. It is a generic (X)Emacs interface for proof assistants, wenzelm@10079: including Isabelle (both for the classic and Isar version). Proof wenzelm@10079: General is suitable for use by pacifists and Emacs militants wenzelm@10079: alike. Its most prominent feature is script management, providing a wenzelm@10079: metaphor of live proof script editing. Proof General has wenzelm@10079: recently gained a rather large following of both beginning and expert wenzelm@10079: users of Isabelle. wenzelm@8809: wenzelm@9927:

wenzelm@8809: wenzelm@11146: Proof General may be used together with the Emacs wenzelm@13141: wenzelm@9927: X-Symbol package, which provides a nice way to get proper wenzelm@9927: mathematical symbols displayed on screen. wenzelm@8809: wenzelm@3306: wenzelm@3259:

Other sources of information

wenzelm@3259: wenzelm@8809:

The Isabelle Page

wenzelm@8809: wenzelm@8809: The Isabelle home page may be accessed both from Cambridge and Munich: wenzelm@8809: wenzelm@8809: wenzelm@8809: wenzelm@8809: wenzelm@3259:

Mailing list

wenzelm@3259: wenzelm@8809: The electronic mailing list isabelle-users@cl.cam.ac.uk wenzelm@3259: provides a forum for Isabelle users to discuss problems and exchange wenzelm@8809: information. To join, send a message to isabelle-users-request@cl.cam.ac.uk. wenzelm@3259: wenzelm@3259: wenzelm@3259:

Personal mail

wenzelm@3259: wenzelm@3259: Lawrence C Paulson
wenzelm@3259: Computer Laboratory
wenzelm@3259: University of Cambridge
wenzelm@3259: Pembroke Street
wenzelm@3259: Cambridge CB2 3QG
wenzelm@3259: England
wenzelm@3259:
oheimb@8068: E-mail: lcp@cl.cam.ac.uk
wenzelm@3259: Phone: +44-223-334600
wenzelm@3259: Fax: +44-223-334748
wenzelm@3259: wenzelm@3259:

wenzelm@3259: or wenzelm@3259:

wenzelm@3259: wenzelm@5401: Tobias Nipkow
wenzelm@9927: Institut für Informatik
wenzelm@9927: T. U. München
wenzelm@9927: D-80290 München
wenzelm@3259: Germany
wenzelm@3259:
oheimb@8068: E-mail: nipkow@in.tum.de
wenzelm@3259: Phone: +49-89-289-22690
wenzelm@3259: Fax: +49-89-289-28183
wenzelm@3259: wenzelm@3259:

wenzelm@3259: wenzelm@3259:

wenzelm@3259: wenzelm@3259: Please report any problems you encounter. While we shall try to be wenzelm@5665: helpful, we can accept no responsibility for the deficiencies of wenzelm@3259: Isabelle and their consequences. wenzelm@3259: wenzelm@3259:
wenzelm@3259: wenzelm@3259: wenzelm@3259: