README
author wenzelm
Wed Jun 09 14:08:08 2010 +0200 (2010-06-09)
changeset 37368 1c816f2abb0e
parent 37159 07f3f5a03e98
child 38470 484e483eb606
permissions -rw-r--r--
removed outdated/confusing INSTALL file;
     1                        The Isabelle System Distribution
     2 
     3 Version information
     4 
     5    This is some unidentified 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-style platform (e.g. Linux,
    13    Windows with Cygwin, Mac OS) and depends on the following main
    14    add-on tools:
    15 
    16      * The Poly/ML compiler and runtime system (version 5.x).
    17      * The GNU bash shell (version 3.x or 2.x).
    18      * Perl (version 5.x).
    19      * GNU Emacs (version 22) -- for the Proof General interface.
    20      * A complete LaTeX installation -- for document preparation.
    21 
    22 Installation
    23 
    24    Completely integrated bundles including the full Isabelle sources,
    25    documentation, add-on tools and precompiled logic images for
    26    several platforms are available from the Isabelle web page.
    27 
    28    Further background information may be found in the Isabelle System
    29    Manual, distributed with the sources (directory doc).
    30 
    31 User interface
    32 
    33    The classic Isabelle user interface is Proof General by David
    34    Aspinall and others. It is a generic Emacs interface for proof
    35    assistants, including Isabelle.  Its most prominent feature is
    36    script management, providing a metaphor of stepwise proof script
    37    editing.  Proof General also provides some support for mathematical
    38    symbols displayed on screen.
    39 
    40 Other sources of information
    41 
    42   The Isabelle Page
    43 
    44    The Isabelle home page may be accessed both from Cambridge and Munich:
    45      * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    46      * http://isabelle.in.tum.de
    47 
    48   Mailing list
    49 
    50    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    51    forum for Isabelle users to discuss problems and exchange
    52    information.  To join, send a message to
    53    isabelle-users-request@cl.cam.ac.uk.
    54 
    55   Personal mail
    56 
    57    Lawrence C Paulson
    58    Computer Laboratory
    59    University of Cambridge
    60    JJ Thomson Avenue
    61    Cambridge CB3 0FD
    62    England
    63    E-mail: lcp@cl.cam.ac.uk
    64    Phone: +44-223-763500
    65    Fax: +44-223-334748
    66 
    67    or
    68 
    69    Tobias Nipkow
    70    Institut fuer Informatik
    71    Technische Universitaet Muenchen
    72    Boltzmannstr. 3
    73    D-85748 Garching
    74    Germany
    75    E-mail: nipkow@in.tum.de
    76    Phone: +49-89-289-17302
    77    Fax: +49-89-289-17307
    78      _________________________________________________________________
    79 
    80    Please report any problems you encounter. While we shall try to be
    81    helpful, we can accept no responsibility for the deficiencies of
    82    Isabelle and their consequences.
    83      _________________________________________________________________