# HG changeset patch
# User wenzelm
# Date 1295208310 -3600
# Node ID e424bc65080d5fd91094f81dd1a0f31a34c9b490
# Parent  d0cced9cdeae15a7f3dd90c980dddc86fc235f12
misc updates for release;

diff -r d0cced9cdeae -r e424bc65080d Admin/CHECKLIST
--- a/Admin/CHECKLIST	Sun Jan 16 20:55:48 2011 +0100
+++ b/Admin/CHECKLIST	Sun Jan 16 21:05:10 2011 +0100
@@ -45,4 +45,3 @@
 - makebundle (multiplatform);
 
 - hdiutil create -srcfolder DIR DMG (Mac OS);
-
diff -r d0cced9cdeae -r e424bc65080d CONTRIBUTORS
--- a/CONTRIBUTORS	Sun Jan 16 20:55:48 2011 +0100
+++ b/CONTRIBUTORS	Sun Jan 16 21:05:10 2011 +0100
@@ -20,20 +20,20 @@
   partial orders in HOL.
 
 * September 2010: Florian Haftmann, TUM
-  Refined concepts for evaluation, i.e., normalisation of terms using
+  Refined concepts for evaluation, i.e., normalization of terms using
   different techniques.
 
 * September 2010: Florian Haftmann, TUM
   Code generation for Scala.
 
 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
-  Rewriting the Probability theory.
+  Improved Probability theory in HOL.
 
 * July 2010: Florian Haftmann, TUM
   Reworking and extension of the Imperative HOL framework.
 
-* July 2010: Alexander Krauss, TUM and Christian Sternagel, University of
-    Innsbruck
+* July 2010: Alexander Krauss, TUM and Christian Sternagel, University
+    of Innsbruck
   Ad-hoc overloading. Generic do notation for monads.
 
 
diff -r d0cced9cdeae -r e424bc65080d README
--- a/README	Sun Jan 16 20:55:48 2011 +0100
+++ b/README	Sun Jan 16 21:05:10 2011 +0100
@@ -17,6 +17,7 @@
      * The GNU bash shell (version 3.x or 2.x).
      * Perl (version 5.x).
      * 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,11 +32,15 @@
 User interface
 
    The classic Isabelle user interface is Proof General by David
-   Aspinall and others. It is a generic Emacs interface for proof
+   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.  Proof General also provides some support for mathematical
-   symbols displayed on screen.
+   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
 
diff -r d0cced9cdeae -r e424bc65080d doc/Contents
--- a/doc/Contents	Sun Jan 16 20:55:48 2011 +0100
+++ b/doc/Contents	Sun Jan 16 21:05:10 2011 +0100
@@ -10,7 +10,7 @@
   sledgehammer    User's Guide to Sledgehammer
   sugar           LaTeX Sugar for Isabelle documents
 
-Reference Manuals
+Main Reference Manuals
   isar-ref        The Isabelle/Isar Reference Manual
   implementation  The Isabelle/Isar Implementation Manual
   system          The Isabelle System Manual