1 The Isabelle System Distribution
5 This is some unidentified repository version of Isabelle.
7 See the NEWS file in the distribution for details on user-relevant
12 Isabelle requires a regular Unix-style platform (e.g. Linux,
13 Windows with Cygwin, Mac OS) and depends on the following main
16 * The Poly/ML compiler and runtime system (version 5.2.1 or later).
17 * The GNU bash shell (version 3.x or 2.x).
19 * GNU Emacs (version 23) -- for the Proof General 4.x interface.
20 * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
21 * A complete LaTeX installation -- for document preparation.
25 Completely integrated bundles including the full Isabelle sources,
26 documentation, add-on tools and precompiled logic images for
27 several platforms are available from the Isabelle web page.
29 Further background information may be found in the Isabelle System
30 Manual, distributed with the sources (directory doc).
34 The classic Isabelle user interface is Proof General by David
35 Aspinall and others. It is a generic Emacs interface for proof
36 assistants, including Isabelle. Its most prominent feature is
37 script management, providing a metaphor of stepwise proof script
40 Isabelle/jEdit is an experimental Prover IDE based on advanced
41 technology of Isabelle/Scala. It provides a metaphor of continuous
42 proof checking of a versioned collection of theory sources, with
43 instantaneous feedback in real-time.
45 Other sources of information
49 The Isabelle home page may be accessed both from Cambridge and Munich:
50 * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
51 * http://isabelle.in.tum.de
55 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
56 forum for Isabelle users to discuss problems and exchange
57 information. To join, send a message to
58 isabelle-users-request@cl.cam.ac.uk.
64 University of Cambridge
68 E-mail: lcp@cl.cam.ac.uk
75 Institut fuer Informatik
76 Technische Universitaet Muenchen
80 E-mail: nipkow@in.tum.de
81 Phone: +49-89-289-17302
83 _________________________________________________________________
85 Please report any problems you encounter. While we shall try to be
86 helpful, we can accept no responsibility for the deficiencies of
87 Isabelle and their consequences.
88 _________________________________________________________________