author | wenzelm |
Mon, 17 Oct 2005 23:10:22 +0200 | |
changeset 17884 | 805eca99d398 |
parent 17883 | efa1bc2bdcc6 |
child 17885 | a1f797ff091e |
src/ZF/Main.thy | file | annotate | diff | comparison | revisions |
--- 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