--- a/README Wed May 12 13:34:24 2010 +0200
+++ b/README Wed May 12 13:52:34 2010 +0200
@@ -12,17 +12,17 @@
Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
following additional software:
- * A full Standard ML Compiler (works best with Poly/ML 5.3.0).
+ * The Poly/ML compiler and runtime system (version 5.x).
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
- * GNU Emacs (version 22 or 23) -- for the Proof General interface.
+ * GNU Emacs (version 22) -- for the Proof General 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, using the tar.gz source distribution. See file
+ platforms from the Isabelle web page. The system may be also built
+ from scratch, using the tar.gz source distribution. See file
INSTALL as distributed with Isabelle for more information.
Further background information may be found in the Isabelle System
@@ -30,13 +30,13 @@
User interface
- The main Isabelle user interface is Proof General by David Aspinall
- and others. It is a generic Emacs interface for proof assistants,
- including Isabelle. 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 also provides some support for mathematical symbols
- displayed on screen.
+ The classic Isabelle user interface is Proof General by David
+ Aspinall and others. It is a generic Emacs interface for proof
+ assistants, including Isabelle. 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 also provides some support for mathematical
+ symbols displayed on screen.
Other sources of information