README
author wenzelm
Mon Nov 12 23:08:12 2007 +0100 (2007-11-12)
changeset 25415 02884a4e1ac6
parent 25214 91730b492a45
child 25447 880419e63924
permissions -rw-r--r--
removed left-over text links from lynx conversion;
removed umlauts (cannot assume iso-latin anymore, and not yet utf-8 either);
haftmann@25214
     1
                       The Isabelle System Distribution
haftmann@25214
     2
haftmann@25214
     3
Version information
haftmann@25214
     4
haftmann@25214
     5
   This is the internal repository version of Isabelle. See the NEWS file
haftmann@25214
     6
   in the distribution for details on user-relevant changes.
haftmann@25214
     7
haftmann@25214
     8
System requirements
haftmann@25214
     9
haftmann@25214
    10
   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
haftmann@25214
    11
   following additional software:
haftmann@25214
    12
     * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).
haftmann@25214
    13
     * The GNU bash shell (version 3.x, 2.x).
haftmann@25214
    14
     * Perl (version 5.x).
wenzelm@25415
    15
     * XEmacs (version 21.4.x) or GNU Emacs (version 21, 22)
wenzelm@25415
    16
       -- for the ProofGeneral interface.
haftmann@25214
    17
     * A complete LaTeX installation -- for document preparation.
haftmann@25214
    18
haftmann@25214
    19
Installation
haftmann@25214
    20
haftmann@25214
    21
   Binary packages are available for Isabelle/HOL and ZF for several
haftmann@25214
    22
   platforms from the Isabelle web page. The system may be easily built
haftmann@25214
    23
   from scratch as well, taking the traditional tar.gz source
haftmann@25214
    24
   distribution. See file INSTALL as distributed with Isabelle for more
haftmann@25214
    25
   information.
haftmann@25214
    26
haftmann@25214
    27
   Further background information may be found in the Isabelle System
haftmann@25214
    28
   Manual, distributed with the sources (directory doc).
haftmann@25214
    29
haftmann@25214
    30
User interface
haftmann@25214
    31
wenzelm@25415
    32
   The canonical Isabelle user interface is Proof General by David
haftmann@25214
    33
   Aspinall and others. It is a generic (X)Emacs interface for proof
haftmann@25214
    34
   assistants, including Isabelle (both for the classic and Isar
haftmann@25214
    35
   version). Proof General is suitable for use by pacifists and Emacs
haftmann@25214
    36
   militants alike. Its most prominent feature is script management,
haftmann@25214
    37
   providing a metaphor of live proof script editing. Proof General has
haftmann@25214
    38
   recently gained a rather large following of both beginning and expert
haftmann@25214
    39
   users of Isabelle.
haftmann@25214
    40
wenzelm@25415
    41
   Proof General is distributed together with the XEmacs X-Symbol
haftmann@25214
    42
   package, which provides a nice way to get proper mathematical symbols
haftmann@25214
    43
   displayed on screen.
haftmann@25214
    44
haftmann@25214
    45
Other sources of information
haftmann@25214
    46
haftmann@25214
    47
  The Isabelle Page
haftmann@25214
    48
haftmann@25214
    49
   The Isabelle home page may be accessed both from Cambridge and Munich:
wenzelm@25415
    50
     * http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
wenzelm@25415
    51
     * http://isabelle.in.tum.de
haftmann@25214
    52
haftmann@25214
    53
  Mailing list
haftmann@25214
    54
haftmann@25214
    55
   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
haftmann@25214
    56
   forum for Isabelle users to discuss problems and exchange information.
wenzelm@25415
    57
   To join, send a message to isabelle-users-request@cl.cam.ac.uk.
haftmann@25214
    58
haftmann@25214
    59
  Personal mail
haftmann@25214
    60
wenzelm@25415
    61
   Lawrence C Paulson
haftmann@25214
    62
   Computer Laboratory
haftmann@25214
    63
   University of Cambridge
haftmann@25214
    64
   JJ Thomson Avenue
haftmann@25214
    65
   Cambridge CB3 0FD
haftmann@25214
    66
   England
wenzelm@25415
    67
   E-mail: lcp@cl.cam.ac.uk
haftmann@25214
    68
   Phone: +44-223-763500
haftmann@25214
    69
   Fax: +44-223-334748
haftmann@25214
    70
haftmann@25214
    71
   or
haftmann@25214
    72
wenzelm@25415
    73
   Tobias Nipkow
wenzelm@25415
    74
   Institut fuer Informatik
wenzelm@25415
    75
   Technische Universitaet Muenchen
haftmann@25214
    76
   Boltzmannstr. 3
haftmann@25214
    77
   D-85748 Garching
haftmann@25214
    78
   Germany
wenzelm@25415
    79
   E-mail: nipkow@in.tum.de
haftmann@25214
    80
   Phone: +49-89-289-17302
haftmann@25214
    81
   Fax: +49-89-289-17307
haftmann@25214
    82
     _________________________________________________________________
haftmann@25214
    83
haftmann@25214
    84
   Please report any problems you encounter. While we shall try to be
haftmann@25214
    85
   helpful, we can accept no responsibility for the deficiencies of
haftmann@25214
    86
   Isabelle and their consequences.
haftmann@25214
    87
     _________________________________________________________________
haftmann@25214
    88