equal
deleted
inserted
replaced
69 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" |
69 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" |
70 by (rule transrec3_def [THEN def_transrec, THEN trans], force) |
70 by (rule transrec3_def [THEN def_transrec, THEN trans], force) |
71 |
71 |
72 |
72 |
73 declaration {* fn _ => |
73 declaration {* fn _ => |
74 Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all))) |
74 Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => |
|
75 map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) |
75 *} |
76 *} |
76 |
77 |
77 end |
78 end |