# HG changeset patch
# User wenzelm
# Date 1238676598 -7200
# Node ID 740517878d601ad18f6b78f42224575ad6041a24
# Parent  a218363290c33ac961bdb02b17fd5c595782069a# Parent  6c6b7a72fa3451092bc264561db20788f2bfdf34
merged

diff -r a218363290c3 -r 740517878d60 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Thu Apr 02 14:39:29 2009 +0200
+++ b/Admin/CHECKLIST	Thu Apr 02 14:49:58 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 a218363290c3 -r 740517878d60 INSTALL
--- a/INSTALL	Thu Apr 02 14:39:29 2009 +0200
+++ b/INSTALL	Thu Apr 02 14:49:58 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 a218363290c3 -r 740517878d60 README
--- a/README	Thu Apr 02 14:39:29 2009 +0200
+++ b/README	Thu Apr 02 14:49:58 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 a218363290c3 -r 740517878d60 doc/Contents
--- a/doc/Contents	Thu Apr 02 14:39:29 2009 +0200
+++ b/doc/Contents	Thu Apr 02 14:49:58 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
diff -r a218363290c3 -r 740517878d60 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Apr 02 14:39:29 2009 +0200
+++ b/src/Pure/pure_thy.ML	Thu Apr 02 14:49:58 2009 +0200
@@ -31,10 +31,10 @@
   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
-  val note_thmss: string -> (Thm.binding *
-      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> (Thm.binding *
-      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
+    -> theory -> (string * thm list) list * theory
+  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
+    -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->