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