isabelle: src/ZF/Main.ML@f8a134b9a57f (annotated)

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
12720 f8a134b9a57f replace gen_all by forall_elim_vars_safe; wenzelm parents: 12715 diff changeset	7	simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o forall_elim_vars_safe);