src/ZF/Main.thy

--- a/src/ZF/Main.thy	Mon Oct 17 23:10:21 2005 +0200
+++ b/src/ZF/Main.thy	Mon Oct 17 23:10:22 2005 +0200
@@ -72,11 +72,8 @@
 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
 
 
-subsection{* Remaining Declarations *}
-
-(* belongs to theory IntDiv *)
-lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
-  and negDivAlg_induct = negDivAlg_induct [consumes 2]
-
+ML_setup {*
+  change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
+*}
 
 end