tuned;

--- a/src/HOL/Product_Type.thy	Sat Oct 27 23:15:52 2001 +0200
+++ b/src/HOL/Product_Type.thy	Sat Oct 27 23:16:15 2001 +0200
@@ -147,7 +147,7 @@
   Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
 
-subsubsection {* Lemmas and tool setup *}
+subsubsection {* Lemmas and proof tool setup *}
 
 lemma ProdI: "Pair_Rep a b : Prod"
   by (unfold Prod_def) blast

--- a/src/Pure/ROOT.ML	Sat Oct 27 23:15:52 2001 +0200
+++ b/src/Pure/ROOT.ML	Sat Oct 27 23:16:15 2001 +0200
@@ -26,7 +26,7 @@
 (*inner syntax module*)
 cd "Syntax"; use "ROOT.ML"; cd "..";
 
-(*main system*)
+(*core system*)
 use "sorts.ML";
 use "type_infer.ML";
 use "type.ML";
@@ -58,11 +58,13 @@
 (*the Isar subsystem*)
 cd "Isar"; use "ROOT.ML"; cd "..";
 
-use "goals.ML";
 use "axclass.ML";
 use "codegen.ML";
 
-(*external interfaces*)
+(*old-style goal package*)
+use "goals.ML";
+
+(*specific support for user-interfaces*)
 cd "Interface"; use "ROOT.ML"; cd "..";
 
 (*final Pure theory setup*)