# HG changeset patch
# User wenzelm
# Date 1129583422 -7200
# Node ID 805eca99d3986df3c5e3595bbe126cfe6ed9ae76
# Parent  efa1bc2bdcc61c3ac54d3ea689b81ea440dfd356
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
change_simpset;

diff -r efa1bc2bdcc6 -r 805eca99d398 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