README
author wenzelm
Fri Apr 27 15:59:50 2012 +0200 (2012-04-27 ago)
changeset 47795 ccb10fe4b955
parent 47745 de249b5ae6e2
child 47805 5d283dca6104
permissions -rw-r--r--
some updates on classic README, reduce the impression that there is much to install manually;
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
wenzelm@47795
    10
Installation
wenzelm@33842
    11
wenzelm@47795
    12
   Isabelle work on the three main platform families: Linux, Mac OS X,
wenzelm@47795
    13
   and Windows (via Cygwin).
haftmann@25214
    14
wenzelm@37368
    15
   Completely integrated bundles including the full Isabelle sources,
wenzelm@37368
    16
   documentation, add-on tools and precompiled logic images for
wenzelm@37368
    17
   several platforms are available from the Isabelle web page.
haftmann@25214
    18
wenzelm@47795
    19
   Some background information may be found in the Isabelle System
haftmann@25214
    20
   Manual, distributed with the sources (directory doc).
haftmann@25214
    21
wenzelm@47795
    22
User interfaces
haftmann@25214
    23
wenzelm@44801
    24
   Isabelle/jEdit is an emerging Prover IDE based on advanced
wenzelm@44801
    25
   technology of Isabelle/Scala.  It provides a metaphor of continuous
wenzelm@44801
    26
   proof checking of a versioned collection of theory sources, with
wenzelm@44801
    27
   instantaneous feedback in real-time and rich semantic markup
wenzelm@44801
    28
   associated with the formal text.
wenzelm@44801
    29
wenzelm@36858
    30
   The classic Isabelle user interface is Proof General by David
wenzelm@41596
    31
   Aspinall and others.  It is a generic Emacs interface for proof
wenzelm@37159
    32
   assistants, including Isabelle.  Its most prominent feature is
wenzelm@37159
    33
   script management, providing a metaphor of stepwise proof script
wenzelm@41596
    34
   editing.
wenzelm@41596
    35
haftmann@25214
    36
Other sources of information
haftmann@25214
    37
haftmann@25214
    38
  The Isabelle Page
haftmann@25214
    39
haftmann@25214
    40
   The Isabelle home page may be accessed both from Cambridge and Munich:
haftmann@27085
    41
     * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
wenzelm@25415
    42
     * http://isabelle.in.tum.de
haftmann@25214
    43
haftmann@25214
    44
  Mailing list
haftmann@25214
    45
haftmann@25214
    46
   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
wenzelm@25447
    47
   forum for Isabelle users to discuss problems and exchange
wenzelm@25447
    48
   information.  To join, send a message to
wenzelm@25447
    49
   isabelle-users-request@cl.cam.ac.uk.
haftmann@25214
    50
haftmann@25214
    51
  Personal mail
haftmann@25214
    52
wenzelm@25415
    53
   Lawrence C Paulson
haftmann@25214
    54
   Computer Laboratory
haftmann@25214
    55
   University of Cambridge
haftmann@25214
    56
   JJ Thomson Avenue
haftmann@25214
    57
   Cambridge CB3 0FD
haftmann@25214
    58
   England
wenzelm@25415
    59
   E-mail: lcp@cl.cam.ac.uk
haftmann@25214
    60
   Phone: +44-223-763500
haftmann@25214
    61
   Fax: +44-223-334748
haftmann@25214
    62
haftmann@25214
    63
   or
haftmann@25214
    64
wenzelm@25415
    65
   Tobias Nipkow
wenzelm@25415
    66
   Institut fuer Informatik
wenzelm@25415
    67
   Technische Universitaet Muenchen
haftmann@25214
    68
   Boltzmannstr. 3
haftmann@25214
    69
   D-85748 Garching
haftmann@25214
    70
   Germany
wenzelm@25415
    71
   E-mail: nipkow@in.tum.de
haftmann@25214
    72
   Phone: +49-89-289-17302
haftmann@25214
    73
   Fax: +49-89-289-17307
haftmann@25214
    74
     _________________________________________________________________
haftmann@25214
    75
haftmann@25214
    76
   Please report any problems you encounter. While we shall try to be
haftmann@25214
    77
   helpful, we can accept no responsibility for the deficiencies of
haftmann@25214
    78
   Isabelle and their consequences.
haftmann@25214
    79
     _________________________________________________________________