README
author wenzelm
Thu, 03 Oct 2013 17:03:20 +0200
changeset 55192 65c6a00ff86b
parent 55188 cdba71c67860
child 55272 6e943f644cca
child 58794 ecad2a53755a
permissions -rw-r--r--
Added tag Isabelle2013-1-RC1 for changeset c37100233af7
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@48668
    10
Installation
haftmann@25214
    11
wenzelm@51587
    12
   Isabelle works on the three main platform families: Linux, Windows,
wenzelm@55115
    13
   and Mac OS X.  The application bundles from the Isabelle web page
wenzelm@55115
    14
   include sources, documentation, and add-on tools for all supported
wenzelm@55115
    15
   platforms.
haftmann@25214
    16
wenzelm@55188
    17
   Some technical background information may be found in the Isabelle
wenzelm@55188
    18
   System Manual (directory doc).
haftmann@25214
    19
wenzelm@48668
    20
User interfaces
haftmann@25214
    21
wenzelm@51587
    22
   Isabelle/jEdit is an advanced Prover IDE based on jEdit and
wenzelm@51587
    23
   Isabelle/Scala.  It provides a metaphor of continuous proof
wenzelm@51587
    24
   checking of a versioned collection of theory sources, with
wenzelm@45682
    25
   instantaneous feedback in real-time and rich semantic markup
wenzelm@45682
    26
   associated with the formal text.
wenzelm@45682
    27
wenzelm@36865
    28
   The classic Isabelle user interface is Proof General by David
wenzelm@41844
    29
   Aspinall and others.  It is a generic Emacs interface for proof
wenzelm@48676
    30
   assistants, including Isabelle.  Its main feature is script
wenzelm@51587
    31
   management, with stepwise proof scripting and partial locking of
wenzelm@51587
    32
   the editor buffer.
wenzelm@41844
    33
haftmann@25214
    34
Other sources of information
haftmann@25214
    35
haftmann@25214
    36
  The Isabelle Page
haftmann@25214
    37
wenzelm@51587
    38
   The Isabelle home page may be accessed from Cambridge, Munich, and
wenzelm@51587
    39
   Sydney:
wenzelm@51587
    40
haftmann@27085
    41
     * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
wenzelm@25415
    42
     * http://isabelle.in.tum.de
wenzelm@51587
    43
     * http://mirror.cse.unsw.edu.au/pub/isabelle/index.html
haftmann@25214
    44
haftmann@25214
    45
  Mailing list
haftmann@25214
    46
haftmann@25214
    47
   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
wenzelm@25447
    48
   forum for Isabelle users to discuss problems and exchange
wenzelm@25447
    49
   information.  To join, send a message to
wenzelm@25447
    50
   isabelle-users-request@cl.cam.ac.uk.
haftmann@25214
    51
haftmann@25214
    52
  Personal mail
haftmann@25214
    53
wenzelm@25415
    54
   Lawrence C Paulson
haftmann@25214
    55
   Computer Laboratory
haftmann@25214
    56
   University of Cambridge
haftmann@25214
    57
   JJ Thomson Avenue
haftmann@25214
    58
   Cambridge CB3 0FD
haftmann@25214
    59
   England
wenzelm@25415
    60
   E-mail: lcp@cl.cam.ac.uk
haftmann@25214
    61
   Phone: +44-223-763500
haftmann@25214
    62
   Fax: +44-223-334748
haftmann@25214
    63
haftmann@25214
    64
   or
haftmann@25214
    65
wenzelm@25415
    66
   Tobias Nipkow
wenzelm@25415
    67
   Institut fuer Informatik
wenzelm@25415
    68
   Technische Universitaet Muenchen
haftmann@25214
    69
   Boltzmannstr. 3
haftmann@25214
    70
   D-85748 Garching
haftmann@25214
    71
   Germany
wenzelm@25415
    72
   E-mail: nipkow@in.tum.de
haftmann@25214
    73
   Phone: +49-89-289-17302
haftmann@25214
    74
   Fax: +49-89-289-17307
haftmann@25214
    75
     _________________________________________________________________
haftmann@25214
    76
haftmann@25214
    77
   Please report any problems you encounter. While we shall try to be
haftmann@25214
    78
   helpful, we can accept no responsibility for the deficiencies of
haftmann@25214
    79
   Isabelle and their consequences.
haftmann@25214
    80
     _________________________________________________________________