The Isabelle System Distribution Version information This is some unidentified repository version of Isabelle. See the NEWS file in the distribution for details on user-relevant changes. System requirements Isabelle requires a regular Unix-style platform (e.g. Linux, Windows with Cygwin, Mac OS X) and depends on the following main add-on tools: * The Poly/ML compiler and runtime system (version 5.2.1 or later). * The GNU bash shell (version 3.x or 2.x). * Perl (version 5.x). * Java 1.6.x from Oracle or Apple -- for Scala and jEdit. * GNU Emacs (version 23) -- for the Proof General 4.x interface. * A complete LaTeX installation -- for document preparation. Installation Completely integrated bundles including the full Isabelle sources, documentation, add-on tools and precompiled logic images for several platforms are available from the Isabelle web page. Further background information may be found in the Isabelle System Manual, distributed with the sources (directory doc). User interface Isabelle/jEdit is an emerging Prover IDE based on advanced technology of Isabelle/Scala. It provides a metaphor of continuous proof checking of a versioned collection of theory sources, with instantaneous feedback in real-time and rich semantic markup associated with the formal text. The classic Isabelle user interface is Proof General by David Aspinall and others. It is a generic Emacs interface for proof assistants, including Isabelle. Its most prominent feature is script management, providing a metaphor of stepwise proof script editing. Other sources of information The Isabelle Page The Isabelle home page may be accessed both from Cambridge and Munich: * http://www.cl.cam.ac.uk/research/hvg/Isabelle/ * http://isabelle.in.tum.de Mailing list The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems and exchange information. To join, send a message to isabelle-users-request@cl.cam.ac.uk. Personal mail Lawrence C Paulson Computer Laboratory University of Cambridge JJ Thomson Avenue Cambridge CB3 0FD England E-mail: lcp@cl.cam.ac.uk Phone: +44-223-763500 Fax: +44-223-334748 or Tobias Nipkow Institut fuer Informatik Technische Universitaet Muenchen Boltzmannstr. 3 D-85748 Garching Germany E-mail: nipkow@in.tum.de Phone: +49-89-289-17302 Fax: +49-89-289-17307 _________________________________________________________________ Please report any problems you encounter. While we shall try to be helpful, we can accept no responsibility for the deficiencies of Isabelle and their consequences. _________________________________________________________________