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: haftmann@25214: Isabelle requires a regular Unix platform (e.g. GNU Linux) with the haftmann@25214: following additional software: wenzelm@30852: * A full Standard ML Compiler (works best with Poly/ML 5.2.1). wenzelm@27006: * The GNU bash shell (version 3.x or 2.x). haftmann@25214: * Perl (version 5.x). wenzelm@30898: * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x) wenzelm@25447: -- for the Proof General interface. haftmann@25214: * A complete LaTeX installation -- for document preparation. haftmann@25214: haftmann@25214: Installation haftmann@25214: haftmann@25214: Binary packages are available for Isabelle/HOL and ZF for several wenzelm@25447: platforms from the Isabelle web page. The system may be easily wenzelm@30898: built from scratch, using the tar.gz source distribution. See file wenzelm@30898: INSTALL as distributed with Isabelle for more information. 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@30852: The main Isabelle user interface is Proof General by David Aspinall wenzelm@30852: and others. It is a generic Emacs interface for proof assistants, wenzelm@30852: including Isabelle. Proof General is suitable for use by pacifists wenzelm@30852: and Emacs militants alike. Its most prominent feature is script wenzelm@30852: management, providing a metaphor of live proof script editing. wenzelm@30898: Proof General also provides some support for mathematical symbols wenzelm@30898: displayed on screen. 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: _________________________________________________________________