src/HOL/ROOT.ML
changeset 5183 89f162de39cf
parent 5124 1ce3cccfacdb
child 5219 924359415f09
     1.1 --- a/src/HOL/ROOT.ML	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -26,8 +26,6 @@
     1.4  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
     1.6  
     1.7 -use "thy_data.ML";
     1.8 -
     1.9  use_thy "HOL";
    1.10  use "hologic.ML";
    1.11  use "cladata.ML";
    1.12 @@ -42,13 +40,21 @@
    1.13  use "Tools/record_package.ML";
    1.14  use_thy "Record";
    1.15  
    1.16 -use "datatype.ML";
    1.17 -use_thy "Arith";
    1.18 -use "arith_data.ML";
    1.19 +use_thy "NatDef";
    1.20  
    1.21  use "Tools/inductive_package.ML";
    1.22  use_thy "Inductive";
    1.23  
    1.24 +use "Tools/datatype_aux.ML";
    1.25 +use "Tools/datatype_prop.ML";
    1.26 +use "Tools/datatype_rep_proofs.ML";
    1.27 +use "Tools/datatype_abs_proofs.ML";
    1.28 +use "Tools/datatype_package.ML";
    1.29 +use "Tools/primrec_package.ML";
    1.30 +
    1.31 +use_thy "Arith";
    1.32 +use "arith_data.ML";
    1.33 +
    1.34  use_thy "RelPow";
    1.35  use_thy "Finite";
    1.36  use_thy "Sexp";