haftmann@25214:                        The Isabelle System Distribution
haftmann@25214: 
haftmann@25214: Version information
haftmann@25214: 
wenzelm@32361:    This is some unidentified repository version of Isabelle.
wenzelm@27646: 
wenzelm@27646:    See the NEWS file in the distribution for details on user-relevant
wenzelm@27646:    changes.
haftmann@25214: 
wenzelm@48668: Installation
haftmann@25214: 
wenzelm@48676:    Isabelle works on the three main platform families: Linux, Mac OS
wenzelm@48676:    X, and Windows (via Cygwin).
haftmann@25214: 
wenzelm@37469:    Completely integrated bundles including the full Isabelle sources,
wenzelm@37469:    documentation, add-on tools and precompiled logic images for
wenzelm@37469:    several platforms are available from the Isabelle web page.
haftmann@25214: 
wenzelm@48668:    Some background information may be found in the Isabelle System
haftmann@25214:    Manual, distributed with the sources (directory doc).
haftmann@25214: 
wenzelm@48668: User interfaces
haftmann@25214: 
wenzelm@45682:    Isabelle/jEdit is an emerging Prover IDE based on advanced
wenzelm@45682:    technology of Isabelle/Scala.  It provides a metaphor of continuous
wenzelm@45682:    proof checking of a versioned collection of theory sources, with
wenzelm@45682:    instantaneous feedback in real-time and rich semantic markup
wenzelm@45682:    associated with the formal text.
wenzelm@45682: 
wenzelm@36865:    The classic Isabelle user interface is Proof General by David
wenzelm@41844:    Aspinall and others.  It is a generic Emacs interface for proof
wenzelm@48676:    assistants, including Isabelle.  Its main feature is script
wenzelm@48676:    management, providing a metaphor of stepwise proof script editing
wenzelm@48676:    and partial locking of the buffer.
wenzelm@41844: 
haftmann@25214: Other sources of information
haftmann@25214: 
haftmann@25214:   The Isabelle Page
haftmann@25214: 
haftmann@25214:    The Isabelle home page may be accessed both from Cambridge and Munich:
haftmann@27085:      * http://www.cl.cam.ac.uk/research/hvg/Isabelle/
wenzelm@25415:      * http://isabelle.in.tum.de
haftmann@25214: 
haftmann@25214:   Mailing list
haftmann@25214: 
haftmann@25214:    The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
wenzelm@25447:    forum for Isabelle users to discuss problems and exchange
wenzelm@25447:    information.  To join, send a message to
wenzelm@25447:    isabelle-users-request@cl.cam.ac.uk.
haftmann@25214: 
haftmann@25214:   Personal mail
haftmann@25214: 
wenzelm@25415:    Lawrence C Paulson
haftmann@25214:    Computer Laboratory
haftmann@25214:    University of Cambridge
haftmann@25214:    JJ Thomson Avenue
haftmann@25214:    Cambridge CB3 0FD
haftmann@25214:    England
wenzelm@25415:    E-mail: lcp@cl.cam.ac.uk
haftmann@25214:    Phone: +44-223-763500
haftmann@25214:    Fax: +44-223-334748
haftmann@25214: 
haftmann@25214:    or
haftmann@25214: 
wenzelm@25415:    Tobias Nipkow
wenzelm@25415:    Institut fuer Informatik
wenzelm@25415:    Technische Universitaet Muenchen
haftmann@25214:    Boltzmannstr. 3
haftmann@25214:    D-85748 Garching
haftmann@25214:    Germany
wenzelm@25415:    E-mail: nipkow@in.tum.de
haftmann@25214:    Phone: +49-89-289-17302
haftmann@25214:    Fax: +49-89-289-17307
haftmann@25214:      _________________________________________________________________
haftmann@25214: 
haftmann@25214:    Please report any problems you encounter. While we shall try to be
haftmann@25214:    helpful, we can accept no responsibility for the deficiencies of
haftmann@25214:    Isabelle and their consequences.
haftmann@25214:      _________________________________________________________________