equal
deleted
inserted
replaced
320 apply(blast) |
320 apply(blast) |
321 apply(blast) |
321 apply(blast) |
322 apply(simp_all add: ty2.distinct) |
322 apply(simp_all add: ty2.distinct) |
323 done |
323 done |
324 |
324 |
325 termination |
325 termination (eqvt) |
326 by lexicographic_order |
326 by lexicographic_order |
327 |
327 |
328 lemma subst_eqvt[eqvt]: |
328 lemma subst_eqvt[eqvt]: |
329 shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)" |
329 shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)" |
330 by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt) |
330 by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt) |