src/ZF/Main.ML
author huffman
Tue, 06 Sep 2005 23:11:09 +0200
changeset 17295 fadf6e1faa16
parent 12725 7ede865e1fe5
child 17876 b9c92f384109
permissions -rw-r--r--
transfer principle tactic


structure Main =
struct
  val thy = the_context ();
end;

simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);