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