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