proper dependencies of all theories and packages;
authorwenzelm
Mon Oct 04 21:45:10 1999 +0200 (1999-10-04)
changeset 77036b3424e877bd
parent 7702 35c7e0df749f
child 7704 9a6783fdb9a5
proper dependencies of all theories and packages;
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Mon Oct 04 21:44:28 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Mon Oct 04 21:45:10 1999 +0200
     1.3 @@ -33,33 +33,7 @@
     1.4  use "~~/src/Provers/quantifier1.ML";
     1.5  use "~~/src/Provers/Arith/combine_coeff.ML";
     1.6  
     1.7 -use_thy "subset";
     1.8 -use "Tools/typedef_package.ML";
     1.9 -use_thy "Inductive";
    1.10 -use_thy "NatDef";
    1.11 -
    1.12 -use "Tools/datatype_aux.ML";
    1.13 -use "Tools/datatype_prop.ML";
    1.14 -use "Tools/datatype_rep_proofs.ML";
    1.15 -use "Tools/datatype_abs_proofs.ML";
    1.16 -use "Tools/datatype_package.ML";
    1.17 -use "Tools/primrec_package.ML";
    1.18 -use_thy "Datatype";
    1.19 -
    1.20 -(*TFL: recursive function definitions*)
    1.21 -use_thy "WF_Rel";
    1.22 -cd "../TFL"; use "sys.sml"; cd "../HOL";
    1.23 -use_thy "Recdef";
    1.24 -
    1.25 -use_thy "Numeral";
    1.26 -cd "Integ";
    1.27 -use_thy "IntDef";
    1.28 -use "simproc.ML";
    1.29 -use_thy "NatBin";
    1.30 -cd "..";
    1.31 -
    1.32 -(*the all-in-one theory*)
    1.33 -use_thy "Main";
    1.34 +with_path "Integ" use_thy "Main";
    1.35  
    1.36  print_depth 8;
    1.37