# HG changeset patch
# User wenzelm
# Date 1238675416 -7200
# Node ID 59a422908e2933ab7ed26939b01983d15cbcab5f
# Parent  0e5ec6d2c1d95abea0372b5c2c8900d588423afe
misc tuning for release;

diff -r 0e5ec6d2c1d9 -r 59a422908e29 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Thu Apr 02 14:09:41 2009 +0200
+++ b/Admin/CHECKLIST	Thu Apr 02 14:30:16 2009 +0200
@@ -20,12 +20,9 @@
     doc/Contents
 
 - maintain Logics:
-    Admin/makedist
     build
     lib/Tools/makeall
-    lib/html/index.html
-    doc-src/Logics/intro.tex
-    doc-src/Logics/logics.tex
+    lib/html/library_index_content.template
 
 - after release: 
     commit new ~isabelle/website/include/documentationdist.include.html to website SVN
diff -r 0e5ec6d2c1d9 -r 59a422908e29 INSTALL
--- a/INSTALL	Thu Apr 02 14:09:41 2009 +0200
+++ b/INSTALL	Thu Apr 02 14:30:16 2009 +0200
@@ -73,7 +73,7 @@
 isabelle-process) directly from their location within the distribution
 directory [ISABELLE_HOME] like this:
 
-  [ISABELLE_HOME]/bin/isabelle-process HOL
+  [ISABELLE_HOME]/bin/isabelle tty -l HOL
 
 This starts an interactive Isabelle session within the current text
 terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
diff -r 0e5ec6d2c1d9 -r 59a422908e29 README
--- a/README	Thu Apr 02 14:09:41 2009 +0200
+++ b/README	Thu Apr 02 14:30:16 2009 +0200
@@ -11,7 +11,7 @@
 
    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.x).
+     * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
      * The GNU bash shell (version 3.x or 2.x).
      * Perl (version 5.x).
      * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
@@ -31,15 +31,12 @@
 
 User interface
 
-   The canonical Isabelle user interface is Proof General by David
-   Aspinall and others. It is a generic (X)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 is distributed together with the XEmacs X-Symbol
-   package, which provides a reasonable way to get proper mathematical
+   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 proper mathematical
    symbols displayed on screen.
 
 Other sources of information
diff -r 0e5ec6d2c1d9 -r 59a422908e29 doc/Contents
--- a/doc/Contents	Thu Apr 02 14:09:41 2009 +0200
+++ b/doc/Contents	Thu Apr 02 14:30:16 2009 +0200
@@ -13,7 +13,7 @@
   implementation  The Isabelle/Isar Implementation Manual
   system          The Isabelle System Manual
 
-Old Manuals (outdated!)
+Old Manuals (outdated)
   intro           Old Introduction to Isabelle
   ref             Old Isabelle Reference Manual
   logics          Isabelle's Logics: overview and misc logics