1.1 --- a/README	Sat Apr 11 10:24:21 2015 +0200
     1.2 +++ b/README	Sat Apr 11 11:28:31 2015 +0200
     1.3 @@ -17,19 +17,15 @@
     1.4     Some technical background information may be found in the Isabelle
     1.5     System Manual (directory doc).
     1.6  
     1.7 -User interfaces
     1.8 +User interface
     1.9  
    1.10     Isabelle/jEdit is an advanced Prover IDE based on jEdit and
    1.11 -   Isabelle/Scala.  It provides a metaphor of continuous proof
    1.12 -   checking of a versioned collection of theory sources, with
    1.13 -   instantaneous feedback in real-time and rich semantic markup
    1.14 -   associated with the formal text.
    1.15 -
    1.16 -   The classic Isabelle user interface is Proof General by David
    1.17 -   Aspinall and others.  It is a generic Emacs interface for proof
    1.18 -   assistants, including Isabelle.  Its main feature is script
    1.19 -   management, with stepwise proof scripting and partial locking of
    1.20 -   the editor buffer.
    1.21 +   Isabelle/Scala.  It is the main example application of the
    1.22 +   Isabelle/PIDE framework, and the default user interface of
    1.23 +   Isabelle.  It provides a metaphor of continuous proof checking of a
    1.24 +   versioned collection of theory sources, with instantaneous feedback
    1.25 +   in real-time and rich semantic markup associated with the formal
    1.26 +   text.
    1.27  
    1.28  Other sources of information
    1.29