src/ZF/ROOT.ML
changeset 12183 c10cea75dd56
parent 12175 5cf58a1799a7
child 12552 d2d2ab3f1f37
     1.1 --- a/src/ZF/ROOT.ML	Wed Nov 14 18:46:07 2001 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Wed Nov 14 18:46:30 2001 +0100
     1.3 @@ -21,14 +21,7 @@
     1.4  use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.5  use "~~/src/Provers/Arith/combine_numerals.ML";
     1.6  
     1.7 -use_thy "mono";
     1.8 -use "ind_syntax.ML";
     1.9 -use_thy "Datatype";
    1.10 -
    1.11 -use     "Tools/numeral_syntax.ML";
    1.12 -(*the all-in-one theory*)
    1.13  with_path "Integ" use_thy "Main";
    1.14 -
    1.15  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    1.16  
    1.17  print_depth 8;