equal
deleted
inserted
replaced
233 |
233 |
234 text {* |
234 text {* |
235 \medskip Theorems about @{text term_map}. |
235 \medskip Theorems about @{text term_map}. |
236 *} |
236 *} |
237 |
237 |
238 declare List_ZF.map_compose [simp] |
238 declare map_compose [simp] |
239 |
239 |
240 lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t" |
240 lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t" |
241 by (induct rule: term_induct_eqn) simp |
241 by (induct rule: term_induct_eqn) simp |
242 |
242 |
243 lemma term_map_compose: |
243 lemma term_map_compose: |