amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
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 X) 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 * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
20 * GNU Emacs (version 23) -- for the Proof General 4.x interface.
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 Isabelle/jEdit is an emerging Prover IDE based on advanced
35 technology of Isabelle/Scala. It provides a metaphor of continuous
36 proof checking of a versioned collection of theory sources, with
37 instantaneous feedback in real-time and rich semantic markup
38 associated with the formal text.
40 The classic Isabelle user interface is Proof General by David
41 Aspinall and others. It is a generic Emacs interface for proof
42 assistants, including Isabelle. Its most prominent feature is
43 script management, providing a metaphor of stepwise proof script
46 Other sources of information
50 The Isabelle home page may be accessed both from Cambridge and Munich:
51 * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
52 * http://isabelle.in.tum.de
56 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
57 forum for Isabelle users to discuss problems and exchange
58 information. To join, send a message to
59 isabelle-users-request@cl.cam.ac.uk.
65 University of Cambridge
69 E-mail: lcp@cl.cam.ac.uk
76 Institut fuer Informatik
77 Technische Universitaet Muenchen
81 E-mail: nipkow@in.tum.de
82 Phone: +49-89-289-17302
84 _________________________________________________________________
86 Please report any problems you encounter. While we shall try to be
87 helpful, we can accept no responsibility for the deficiencies of
88 Isabelle and their consequences.
89 _________________________________________________________________