src/ZF/ROOT.ML
changeset 8127 68c6159440f1
parent 6349 f7750d816c21
child 8812 7239b21e2068
     1.1 --- a/src/ZF/ROOT.ML	Thu Jan 13 17:36:02 2000 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
     1.3 @@ -44,6 +44,8 @@
     1.4  (*the all-in-one theory*)
     1.5  use_thy "Main";
     1.6  
     1.7 +simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
     1.8 +
     1.9  print_depth 8;
    1.10  
    1.11  Goal "True";  (*leave subgoal package empty*)