README
changeset 25214 91730b492a45
child 25415 02884a4e1ac6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/README	Sat Oct 27 12:48:44 2007 +0200
     1.3 @@ -0,0 +1,87 @@
     1.4 +                       The Isabelle System Distribution
     1.5 +
     1.6 +Version information
     1.7 +
     1.8 +   This is the internal repository version of Isabelle. See the NEWS file
     1.9 +   in the distribution for details on user-relevant changes.
    1.10 +
    1.11 +System requirements
    1.12 +
    1.13 +   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
    1.14 +   following additional software:
    1.15 +     * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).
    1.16 +     * The GNU bash shell (version 3.x, 2.x).
    1.17 +     * Perl (version 5.x).
    1.18 +     * XEmacs (version 21.4.x) -- for the ProofGeneral interface.
    1.19 +     * A complete LaTeX installation -- for document preparation.
    1.20 +
    1.21 +Installation
    1.22 +
    1.23 +   Binary packages are available for Isabelle/HOL and ZF for several
    1.24 +   platforms from the Isabelle web page. The system may be easily built
    1.25 +   from scratch as well, taking the traditional tar.gz source
    1.26 +   distribution. See file INSTALL as distributed with Isabelle for more
    1.27 +   information.
    1.28 +
    1.29 +   Further background information may be found in the Isabelle System
    1.30 +   Manual, distributed with the sources (directory doc).
    1.31 +
    1.32 +User interface
    1.33 +
    1.34 +   The canonical Isabelle user interface is [1]Proof General by David
    1.35 +   Aspinall and others. It is a generic (X)Emacs interface for proof
    1.36 +   assistants, including Isabelle (both for the classic and Isar
    1.37 +   version). Proof General is suitable for use by pacifists and Emacs
    1.38 +   militants alike. Its most prominent feature is script management,
    1.39 +   providing a metaphor of live proof script editing. Proof General has
    1.40 +   recently gained a rather large following of both beginning and expert
    1.41 +   users of Isabelle.
    1.42 +
    1.43 +   Proof General is distributed together with the XEmacs [2]X-Symbol
    1.44 +   package, which provides a nice way to get proper mathematical symbols
    1.45 +   displayed on screen.
    1.46 +
    1.47 +Other sources of information
    1.48 +
    1.49 +  The Isabelle Page
    1.50 +
    1.51 +   The Isabelle home page may be accessed both from Cambridge and Munich:
    1.52 +     * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
    1.53 +     * [4]http://isabelle.in.tum.de
    1.54 +
    1.55 +  Mailing list
    1.56 +
    1.57 +   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    1.58 +   forum for Isabelle users to discuss problems and exchange information.
    1.59 +   To join, send a message to [5]isabelle-users-request@cl.cam.ac.uk.
    1.60 +
    1.61 +  Personal mail
    1.62 +
    1.63 +   [6]Lawrence C Paulson
    1.64 +   Computer Laboratory
    1.65 +   University of Cambridge
    1.66 +   JJ Thomson Avenue
    1.67 +   Cambridge CB3 0FD
    1.68 +   England
    1.69 +   E-mail: [7]lcp@cl.cam.ac.uk
    1.70 +   Phone: +44-223-763500
    1.71 +   Fax: +44-223-334748
    1.72 +
    1.73 +   or
    1.74 +
    1.75 +   [8]Tobias Nipkow
    1.76 +   Institut für Informatik
    1.77 +   Technische Universität München
    1.78 +   Boltzmannstr. 3
    1.79 +   D-85748 Garching
    1.80 +   Germany
    1.81 +   E-mail: [9]nipkow@in.tum.de
    1.82 +   Phone: +49-89-289-17302
    1.83 +   Fax: +49-89-289-17307
    1.84 +     _________________________________________________________________
    1.85 +
    1.86 +   Please report any problems you encounter. While we shall try to be
    1.87 +   helpful, we can accept no responsibility for the deficiencies of
    1.88 +   Isabelle and their consequences.
    1.89 +     _________________________________________________________________
    1.90 +