src/ZF/Main.ML
changeset 12715 f7299128cd7d
parent 12425 97975229f893
child 12720 f8a134b9a57f
equal deleted inserted replaced
12714:61af28328417 12715:f7299128cd7d
     1 
     1 
     2 structure Main =
     2 structure Main =
     3 struct
     3 struct
     4   val thy = the_context ();
     4   val thy = the_context ();
     5 end;
     5 end;
       
     6 
       
     7 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);