README
author blanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 47933 4e8e0245e8be
parent 47805 5d283dca6104
child 50572 b33912e68b84
permissions -rw-r--r--
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
     1                        The Isabelle System Distribution
     2 
     3 Version information
     4 
     5    This is some unidentified repository version of Isabelle.
     6 
     7    See the NEWS file in the distribution for details on user-relevant
     8    changes.
     9 
    10 Installation
    11 
    12    Isabelle works on the three main platform families: Linux, Mac OS
    13    X, and Windows (via Cygwin).
    14 
    15    Completely integrated bundles including the full Isabelle sources,
    16    documentation, add-on tools and precompiled logic images for
    17    several platforms are available from the Isabelle web page.
    18 
    19    Some background information may be found in the Isabelle System
    20    Manual, distributed with the sources (directory doc).
    21 
    22 User interfaces
    23 
    24    Isabelle/jEdit is an emerging Prover IDE based on advanced
    25    technology of Isabelle/Scala.  It provides a metaphor of continuous
    26    proof checking of a versioned collection of theory sources, with
    27    instantaneous feedback in real-time and rich semantic markup
    28    associated with the formal text.
    29 
    30    The classic Isabelle user interface is Proof General by David
    31    Aspinall and others.  It is a generic Emacs interface for proof
    32    assistants, including Isabelle.  Its main feature is script
    33    management, providing a metaphor of stepwise proof script editing
    34    and partial locking of the buffer.
    35 
    36 Other sources of information
    37 
    38   The Isabelle Page
    39 
    40    The Isabelle home page may be accessed both from Cambridge and Munich:
    41      * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    42      * http://isabelle.in.tum.de
    43 
    44   Mailing list
    45 
    46    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    47    forum for Isabelle users to discuss problems and exchange
    48    information.  To join, send a message to
    49    isabelle-users-request@cl.cam.ac.uk.
    50 
    51   Personal mail
    52 
    53    Lawrence C Paulson
    54    Computer Laboratory
    55    University of Cambridge
    56    JJ Thomson Avenue
    57    Cambridge CB3 0FD
    58    England
    59    E-mail: lcp@cl.cam.ac.uk
    60    Phone: +44-223-763500
    61    Fax: +44-223-334748
    62 
    63    or
    64 
    65    Tobias Nipkow
    66    Institut fuer Informatik
    67    Technische Universitaet Muenchen
    68    Boltzmannstr. 3
    69    D-85748 Garching
    70    Germany
    71    E-mail: nipkow@in.tum.de
    72    Phone: +49-89-289-17302
    73    Fax: +49-89-289-17307
    74      _________________________________________________________________
    75 
    76    Please report any problems you encounter. While we shall try to be
    77    helpful, we can accept no responsibility for the deficiencies of
    78    Isabelle and their consequences.
    79      _________________________________________________________________