README
changeset 44801 a0459c50cfc9
parent 41596 e424bc65080d
child 44971 8104eec1bf94
--- a/README	Wed Sep 07 20:29:54 2011 +0200
+++ b/README	Wed Sep 07 20:49:45 2011 +0200
@@ -16,8 +16,8 @@
      * The Poly/ML compiler and runtime system (version 5.2.1 or later).
      * The GNU bash shell (version 3.x or 2.x).
      * Perl (version 5.x).
+     * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
      * GNU Emacs (version 23) -- for the Proof General 4.x interface.
-     * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
      * A complete LaTeX installation -- for document preparation.
 
 Installation
@@ -31,17 +31,18 @@
 
 User interface
 
+   Isabelle/jEdit is an emerging Prover IDE based on advanced
+   technology of Isabelle/Scala.  It provides a metaphor of continuous
+   proof checking of a versioned collection of theory sources, with
+   instantaneous feedback in real-time and rich semantic markup
+   associated with the formal text.
+
    The classic Isabelle user interface is Proof General by David
    Aspinall and others.  It is a generic Emacs interface for proof
    assistants, including Isabelle.  Its most prominent feature is
    script management, providing a metaphor of stepwise proof script
    editing.
 
-   Isabelle/jEdit is an experimental Prover IDE based on advanced
-   technology of Isabelle/Scala.  It provides a metaphor of continuous
-   proof checking of a versioned collection of theory sources, with
-   instantaneous feedback in real-time.
-
 Other sources of information
 
   The Isabelle Page