src/ZF/ROOT.ML
changeset 12552 d2d2ab3f1f37
parent 12183 c10cea75dd56
child 12715 f7299128cd7d
     1.1 --- a/src/ZF/ROOT.ML	Wed Dec 19 11:07:38 2001 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Wed Dec 19 11:13:27 2001 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.5  use "~~/src/Provers/Arith/combine_numerals.ML";
     1.6  
     1.7 -with_path "Integ" use_thy "Main";
     1.8 +with_path "Integ" use_thy "Main_ZFC";
     1.9  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    1.10  
    1.11  print_depth 8;