tuned;
authorwenzelm
Sat Oct 27 23:16:15 2001 +0200 (2001-10-27)
changeset 119668fe2ee787608
parent 11965 c84eb86d9a5f
child 11967 49c7f03cd311
tuned;
src/HOL/Product_Type.thy
src/Pure/ROOT.ML
     1.1 --- a/src/HOL/Product_Type.thy	Sat Oct 27 23:15:52 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Oct 27 23:16:15 2001 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
     1.5  
     1.6  
     1.7 -subsubsection {* Lemmas and tool setup *}
     1.8 +subsubsection {* Lemmas and proof tool setup *}
     1.9  
    1.10  lemma ProdI: "Pair_Rep a b : Prod"
    1.11    by (unfold Prod_def) blast
     2.1 --- a/src/Pure/ROOT.ML	Sat Oct 27 23:15:52 2001 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sat Oct 27 23:16:15 2001 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  (*inner syntax module*)
     2.5  cd "Syntax"; use "ROOT.ML"; cd "..";
     2.6  
     2.7 -(*main system*)
     2.8 +(*core system*)
     2.9  use "sorts.ML";
    2.10  use "type_infer.ML";
    2.11  use "type.ML";
    2.12 @@ -58,11 +58,13 @@
    2.13  (*the Isar subsystem*)
    2.14  cd "Isar"; use "ROOT.ML"; cd "..";
    2.15  
    2.16 -use "goals.ML";
    2.17  use "axclass.ML";
    2.18  use "codegen.ML";
    2.19  
    2.20 -(*external interfaces*)
    2.21 +(*old-style goal package*)
    2.22 +use "goals.ML";
    2.23 +
    2.24 +(*specific support for user-interfaces*)
    2.25  cd "Interface"; use "ROOT.ML"; cd "..";
    2.26  
    2.27  (*final Pure theory setup*)