src/ZF/Main.ML
author wenzelm
Tue, 15 Jan 2002 00:13:20 +0100
changeset 12761 b0c39f9837af
parent 12725 7ede865e1fe5
child 17876 b9c92f384109
permissions -rw-r--r--
save: be slightly more about absent tags; get/add: missing case_names default to numbers 1, 2, 3, ...;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12425
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset
     1
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset
     2
structure Main =
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset
     3
struct
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset
     4
  val thy = the_context ();
97975229f893 added Main.ML;
wenzelm
parents:
diff changeset
     5
end;
12715
f7299128cd7d moved setmksimps to Main!
wenzelm
parents: 12425
diff changeset
     6
12725
7ede865e1fe5 renamed forall_elim_vars_safe to gen_all;
wenzelm
parents: 12720
diff changeset
     7
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);