# 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