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 (fn ss => ss setmksimps (K (map mk_eq o Ord_atomize o gen_all))) |
74 Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all))) |
75 *} |
75 *} |
76 |
76 |
77 end |
77 end |