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