README

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Sat Oct 27 12:48:44 2007 +0200
@@ -0,0 +1,87 @@
+                       The Isabelle System Distribution
+
+Version information
+
+   This is the internal repository version of Isabelle. See the NEWS file
+   in the distribution for details on user-relevant changes.
+
+System requirements
+
+   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
+   following additional software:
+     * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).
+     * The GNU bash shell (version 3.x, 2.x).
+     * Perl (version 5.x).
+     * XEmacs (version 21.4.x) -- for the ProofGeneral interface.
+     * A complete LaTeX installation -- for document preparation.
+
+Installation
+
+   Binary packages are available for Isabelle/HOL and ZF for several
+   platforms from the Isabelle web page. The system may be easily built
+   from scratch as well, taking the traditional tar.gz source
+   distribution. See file INSTALL as distributed with Isabelle for more
+   information.
+
+   Further background information may be found in the Isabelle System
+   Manual, distributed with the sources (directory doc).
+
+User interface
+
+   The canonical Isabelle user interface is [1]Proof General by David
+   Aspinall and others. It is a generic (X)Emacs interface for proof
+   assistants, including Isabelle (both for the classic and Isar
+   version). Proof General is suitable for use by pacifists and Emacs
+   militants alike. Its most prominent feature is script management,
+   providing a metaphor of live proof script editing. Proof General has
+   recently gained a rather large following of both beginning and expert
+   users of Isabelle.
+
+   Proof General is distributed together with the XEmacs [2]X-Symbol
+   package, which provides a nice way to get proper mathematical symbols
+   displayed on screen.
+
+Other sources of information
+
+  The Isabelle Page
+
+   The Isabelle home page may be accessed both from Cambridge and Munich:
+     * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
+     * [4]http://isabelle.in.tum.de
+
+  Mailing list
+
+   The electronic mailing list [e-mail] provides a
+   forum for Isabelle users to discuss problems and exchange information.
+   To join, send a message to [5][e-mail].
+
+  Personal mail
+
+   [6]Lawrence C Paulson
+   Computer Laboratory
+   University of Cambridge
+   JJ Thomson Avenue
+   Cambridge CB3 0FD
+   England
+   E-mail: [7][e-mail]
+   Phone: [phone]
+   Fax: [phone]
+
+   or
+
+   [8]Tobias Nipkow
+   Institut für Informatik
+   Technische Universität München
+   Boltzmannstr. 3
+   D-85748 Garching
+   Germany
+   E-mail: [9][e-mail]
+   Phone: [phone]
+   Fax: [phone]
+     _________________________________________________________________
+
+   Please report any problems you encounter. While we shall try to be
+   helpful, we can accept no responsibility for the deficiencies of
+   Isabelle and their consequences.
+     _________________________________________________________________
+