moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
authorwenzelm
Mon, 17 Oct 2005 23:10:22 +0200
changeset 17884 805eca99d398
parent 17883 efa1bc2bdcc6
child 17885 a1f797ff091e
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy; change_simpset;
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