README
author wenzelm
Wed May 28 22:54:05 2008 +0200 (2008-05-28)
changeset 27006 6ca0c942a25c
parent 25447 880419e63924
child 27085 dbf4f791953d
permissions -rw-r--r--
tuned version numbers;
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:
wenzelm@27006
    12
     * A full Standard ML Compiler (works best with Poly/ML 5.x).
wenzelm@27006
    13
     * The GNU bash shell (version 3.x or 2.x).
haftmann@25214
    14
     * Perl (version 5.x).
wenzelm@27006
    15
     * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
wenzelm@25447
    16
       -- for the Proof General 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
wenzelm@25447
    22
   platforms from the Isabelle web page. The system may be easily
wenzelm@25447
    23
   built from scratch as well, taking the traditional tar.gz source
wenzelm@25447
    24
   distribution. See file INSTALL as distributed with Isabelle for
wenzelm@25447
    25
   more 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
wenzelm@25447
    34
   assistants, including Isabelle. Proof General is suitable for use
wenzelm@25447
    35
   by pacifists and Emacs militants alike. Its most prominent feature
wenzelm@25447
    36
   is script management, providing a metaphor of live proof script
wenzelm@25447
    37
   editing.
haftmann@25214
    38
wenzelm@25415
    39
   Proof General is distributed together with the XEmacs X-Symbol
wenzelm@25447
    40
   package, which provides a reasonable way to get proper mathematical
wenzelm@25447
    41
   symbols displayed on screen.
haftmann@25214
    42
haftmann@25214
    43
Other sources of information
haftmann@25214
    44
haftmann@25214
    45
  The Isabelle Page
haftmann@25214
    46
haftmann@25214
    47
   The Isabelle home page may be accessed both from Cambridge and Munich:
wenzelm@25415
    48
     * http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
wenzelm@25415
    49
     * http://isabelle.in.tum.de
haftmann@25214
    50
haftmann@25214
    51
  Mailing list
haftmann@25214
    52
haftmann@25214
    53
   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
wenzelm@25447
    54
   forum for Isabelle users to discuss problems and exchange
wenzelm@25447
    55
   information.  To join, send a message to
wenzelm@25447
    56
   isabelle-users-request@cl.cam.ac.uk.
haftmann@25214
    57
haftmann@25214
    58
  Personal mail
haftmann@25214
    59
wenzelm@25415
    60
   Lawrence C Paulson
haftmann@25214
    61
   Computer Laboratory
haftmann@25214
    62
   University of Cambridge
haftmann@25214
    63
   JJ Thomson Avenue
haftmann@25214
    64
   Cambridge CB3 0FD
haftmann@25214
    65
   England
wenzelm@25415
    66
   E-mail: lcp@cl.cam.ac.uk
haftmann@25214
    67
   Phone: +44-223-763500
haftmann@25214
    68
   Fax: +44-223-334748
haftmann@25214
    69
haftmann@25214
    70
   or
haftmann@25214
    71
wenzelm@25415
    72
   Tobias Nipkow
wenzelm@25415
    73
   Institut fuer Informatik
wenzelm@25415
    74
   Technische Universitaet Muenchen
haftmann@25214
    75
   Boltzmannstr. 3
haftmann@25214
    76
   D-85748 Garching
haftmann@25214
    77
   Germany
wenzelm@25415
    78
   E-mail: nipkow@in.tum.de
haftmann@25214
    79
   Phone: +49-89-289-17302
haftmann@25214
    80
   Fax: +49-89-289-17307
haftmann@25214
    81
     _________________________________________________________________
haftmann@25214
    82
haftmann@25214
    83
   Please report any problems you encounter. While we shall try to be
haftmann@25214
    84
   helpful, we can accept no responsibility for the deficiencies of
haftmann@25214
    85
   Isabelle and their consequences.
haftmann@25214
    86
     _________________________________________________________________