1 The Isabelle System Distribution
5 This is the internal repository version of Isabelle.
7 See the NEWS file in the distribution for details on user-relevant
12 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
13 following additional software:
14 * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
15 * The GNU bash shell (version 3.x or 2.x).
17 * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
18 -- for the Proof General interface.
19 * A complete LaTeX installation -- for document preparation.
23 Binary packages are available for Isabelle/HOL and ZF for several
24 platforms from the Isabelle web page. The system may be easily
25 built from scratch as well, taking the traditional tar.gz source
26 distribution. See file INSTALL as distributed with Isabelle for
29 Further background information may be found in the Isabelle System
30 Manual, distributed with the sources (directory doc).
34 The main Isabelle user interface is Proof General by David Aspinall
35 and others. It is a generic Emacs interface for proof assistants,
36 including Isabelle. Proof General is suitable for use by pacifists
37 and Emacs militants alike. Its most prominent feature is script
38 management, providing a metaphor of live proof script editing.
39 Proof General also provides some support for proper mathematical
40 symbols displayed on screen.
42 Other sources of information
46 The Isabelle home page may be accessed both from Cambridge and Munich:
47 * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
48 * http://isabelle.in.tum.de
52 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
53 forum for Isabelle users to discuss problems and exchange
54 information. To join, send a message to
55 isabelle-users-request@cl.cam.ac.uk.
61 University of Cambridge
65 E-mail: lcp@cl.cam.ac.uk
72 Institut fuer Informatik
73 Technische Universitaet Muenchen
77 E-mail: nipkow@in.tum.de
78 Phone: +49-89-289-17302
80 _________________________________________________________________
82 Please report any problems you encounter. While we shall try to be
83 helpful, we can accept no responsibility for the deficiencies of
84 Isabelle and their consequences.
85 _________________________________________________________________