moved setmksimps to Main!
authorwenzelm
Fri Jan 11 00:34:43 2002 +0100 (2002-01-11)
changeset 12715f7299128cd7d
parent 12714 61af28328417
child 12716 fa4ea2856a31
moved setmksimps to Main!
src/ZF/Main.ML
src/ZF/ROOT.ML
     1.1 --- a/src/ZF/Main.ML	Fri Jan 11 00:33:35 2002 +0100
     1.2 +++ b/src/ZF/Main.ML	Fri Jan 11 00:34:43 2002 +0100
     1.3 @@ -3,3 +3,5 @@
     1.4  struct
     1.5    val thy = the_context ();
     1.6  end;
     1.7 +
     1.8 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     2.1 --- a/src/ZF/ROOT.ML	Fri Jan 11 00:33:35 2002 +0100
     2.2 +++ b/src/ZF/ROOT.ML	Fri Jan 11 00:34:43 2002 +0100
     2.3 @@ -22,7 +22,6 @@
     2.4  use "~~/src/Provers/Arith/combine_numerals.ML";
     2.5  
     2.6  with_path "Integ" use_thy "Main_ZFC";
     2.7 -simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     2.8  
     2.9  print_depth 8;
    2.10