README
author wenzelm
Thu Apr 02 14:30:16 2009 +0200 (2009-04-02)
changeset 30852 59a422908e29
parent 27646 d010fc1d3c46
child 30898 16912b4e6625
permissions -rw-r--r--
misc tuning for release;
     1                        The Isabelle System Distribution
     2 
     3 Version information
     4 
     5    This is the internal repository version of Isabelle.
     6 
     7    See the NEWS file in the distribution for details on user-relevant
     8    changes.
     9 
    10 System requirements
    11 
    12    Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
    13    following additional software:
    14      * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
    15      * The GNU bash shell (version 3.x or 2.x).
    16      * Perl (version 5.x).
    17      * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
    18        -- for the Proof General interface.
    19      * A complete LaTeX installation -- for document preparation.
    20 
    21 Installation
    22 
    23    Binary packages are available for Isabelle/HOL and ZF for several
    24    platforms from the Isabelle web page. The system may be easily
    25    built from scratch as well, taking the traditional tar.gz source
    26    distribution. See file INSTALL as distributed with Isabelle for
    27    more information.
    28 
    29    Further background information may be found in the Isabelle System
    30    Manual, distributed with the sources (directory doc).
    31 
    32 User interface
    33 
    34    The main Isabelle user interface is Proof General by David Aspinall
    35    and others. It is a generic Emacs interface for proof assistants,
    36    including Isabelle. Proof General is suitable for use by pacifists
    37    and Emacs militants alike. Its most prominent feature is script
    38    management, providing a metaphor of live proof script editing.
    39    Proof General also provides some support for proper mathematical
    40    symbols displayed on screen.
    41 
    42 Other sources of information
    43 
    44   The Isabelle Page
    45 
    46    The Isabelle home page may be accessed both from Cambridge and Munich:
    47      * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    48      * http://isabelle.in.tum.de
    49 
    50   Mailing list
    51 
    52    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    53    forum for Isabelle users to discuss problems and exchange
    54    information.  To join, send a message to
    55    isabelle-users-request@cl.cam.ac.uk.
    56 
    57   Personal mail
    58 
    59    Lawrence C Paulson
    60    Computer Laboratory
    61    University of Cambridge
    62    JJ Thomson Avenue
    63    Cambridge CB3 0FD
    64    England
    65    E-mail: lcp@cl.cam.ac.uk
    66    Phone: +44-223-763500
    67    Fax: +44-223-334748
    68 
    69    or
    70 
    71    Tobias Nipkow
    72    Institut fuer Informatik
    73    Technische Universitaet Muenchen
    74    Boltzmannstr. 3
    75    D-85748 Garching
    76    Germany
    77    E-mail: nipkow@in.tum.de
    78    Phone: +49-89-289-17302
    79    Fax: +49-89-289-17307
    80      _________________________________________________________________
    81 
    82    Please report any problems you encounter. While we shall try to be
    83    helpful, we can accept no responsibility for the deficiencies of
    84    Isabelle and their consequences.
    85      _________________________________________________________________