README
author wenzelm
Mon Sep 19 12:58:52 2011 +0200 (2011-09-19)
changeset 44985 272e8e4e4fc7
parent 44971 8104eec1bf94
child 47462 8f85051693d1
permissions -rw-r--r--
imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;
haftmann@25214
     1
                       The Isabelle System Distribution
haftmann@25214
     2
haftmann@25214
     3
Version information
haftmann@25214
     4
wenzelm@32361
     5
   This is some unidentified repository version of Isabelle.
wenzelm@27646
     6
wenzelm@27646
     7
   See the NEWS file in the distribution for details on user-relevant
wenzelm@27646
     8
   changes.
haftmann@25214
     9
haftmann@25214
    10
System requirements
haftmann@25214
    11
wenzelm@37159
    12
   Isabelle requires a regular Unix-style platform (e.g. Linux,
wenzelm@44971
    13
   Windows with Cygwin, Mac OS X) and depends on the following main
wenzelm@37159
    14
   add-on tools:
wenzelm@33842
    15
wenzelm@38470
    16
     * The Poly/ML compiler and runtime system (version 5.2.1 or later).
wenzelm@27006
    17
     * The GNU bash shell (version 3.x or 2.x).
haftmann@25214
    18
     * Perl (version 5.x).
wenzelm@44801
    19
     * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
wenzelm@41527
    20
     * GNU Emacs (version 23) -- for the Proof General 4.x interface.
haftmann@25214
    21
     * A complete LaTeX installation -- for document preparation.
haftmann@25214
    22
haftmann@25214
    23
Installation
haftmann@25214
    24
wenzelm@37368
    25
   Completely integrated bundles including the full Isabelle sources,
wenzelm@37368
    26
   documentation, add-on tools and precompiled logic images for
wenzelm@37368
    27
   several platforms are available from the Isabelle web page.
haftmann@25214
    28
haftmann@25214
    29
   Further background information may be found in the Isabelle System
haftmann@25214
    30
   Manual, distributed with the sources (directory doc).
haftmann@25214
    31
haftmann@25214
    32
User interface
haftmann@25214
    33
wenzelm@44801
    34
   Isabelle/jEdit is an emerging Prover IDE based on advanced
wenzelm@44801
    35
   technology of Isabelle/Scala.  It provides a metaphor of continuous
wenzelm@44801
    36
   proof checking of a versioned collection of theory sources, with
wenzelm@44801
    37
   instantaneous feedback in real-time and rich semantic markup
wenzelm@44801
    38
   associated with the formal text.
wenzelm@44801
    39
wenzelm@36858
    40
   The classic Isabelle user interface is Proof General by David
wenzelm@41596
    41
   Aspinall and others.  It is a generic Emacs interface for proof
wenzelm@37159
    42
   assistants, including Isabelle.  Its most prominent feature is
wenzelm@37159
    43
   script management, providing a metaphor of stepwise proof script
wenzelm@41596
    44
   editing.
wenzelm@41596
    45
haftmann@25214
    46
Other sources of information
haftmann@25214
    47
haftmann@25214
    48
  The Isabelle Page
haftmann@25214
    49
haftmann@25214
    50
   The Isabelle home page may be accessed both from Cambridge and Munich:
haftmann@27085
    51
     * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
wenzelm@25415
    52
     * http://isabelle.in.tum.de
haftmann@25214
    53
haftmann@25214
    54
  Mailing list
haftmann@25214
    55
haftmann@25214
    56
   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
wenzelm@25447
    57
   forum for Isabelle users to discuss problems and exchange
wenzelm@25447
    58
   information.  To join, send a message to
wenzelm@25447
    59
   isabelle-users-request@cl.cam.ac.uk.
haftmann@25214
    60
haftmann@25214
    61
  Personal mail
haftmann@25214
    62
wenzelm@25415
    63
   Lawrence C Paulson
haftmann@25214
    64
   Computer Laboratory
haftmann@25214
    65
   University of Cambridge
haftmann@25214
    66
   JJ Thomson Avenue
haftmann@25214
    67
   Cambridge CB3 0FD
haftmann@25214
    68
   England
wenzelm@25415
    69
   E-mail: lcp@cl.cam.ac.uk
haftmann@25214
    70
   Phone: +44-223-763500
haftmann@25214
    71
   Fax: +44-223-334748
haftmann@25214
    72
haftmann@25214
    73
   or
haftmann@25214
    74
wenzelm@25415
    75
   Tobias Nipkow
wenzelm@25415
    76
   Institut fuer Informatik
wenzelm@25415
    77
   Technische Universitaet Muenchen
haftmann@25214
    78
   Boltzmannstr. 3
haftmann@25214
    79
   D-85748 Garching
haftmann@25214
    80
   Germany
wenzelm@25415
    81
   E-mail: nipkow@in.tum.de
haftmann@25214
    82
   Phone: +49-89-289-17302
haftmann@25214
    83
   Fax: +49-89-289-17307
haftmann@25214
    84
     _________________________________________________________________
haftmann@25214
    85
haftmann@25214
    86
   Please report any problems you encounter. While we shall try to be
haftmann@25214
    87
   helpful, we can accept no responsibility for the deficiencies of
haftmann@25214
    88
   Isabelle and their consequences.
haftmann@25214
    89
     _________________________________________________________________