src/ZF/Main_ZF.thy
changeset 26339 7825c83c9eff
parent 26056 6a0801279f4c
child 29580 117b88da143c
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
    70      "Limit(i) ==> 
    70      "Limit(i) ==> 
    71       transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
    71       transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
    72 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
    72 by (rule transrec3_def [THEN def_transrec, THEN trans], force)
    73 
    73 
    74 
    74 
    75 ML_setup {*
    75 declaration {* fn _ =>
    76   change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
    76   Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    77 *}
    77 *}
    78 
    78 
    79 end
    79 end