src/ZF/ROOT.ML
changeset 12715 f7299128cd7d
parent 12552 d2d2ab3f1f37
child 15481 fc075ae929e4
     1.1 --- a/src/ZF/ROOT.ML	Fri Jan 11 00:33:35 2002 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Jan 11 00:34:43 2002 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4  use "~~/src/Provers/Arith/combine_numerals.ML";
     1.5  
     1.6  with_path "Integ" use_thy "Main_ZFC";
     1.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     1.8  
     1.9  print_depth 8;
    1.10