| changeset 18348 | b5d7649f8aca |
| parent 18345 | d37fb71754fe |
| child 18378 | 35fba71ec6ef |
| 18347:18568b35035a | 18348:b5d7649f8aca |
|---|---|
884 apply(atomize) |
884 apply(atomize) |
885 apply(force dest!: t2_elim) |
885 apply(force dest!: t2_elim) |
886 (* Abstractions *) |
886 (* Abstractions *) |
887 apply(auto dest!: t3_elim simp only: psubst_Lam) |
887 apply(auto dest!: t3_elim simp only: psubst_Lam) |
888 apply(rule abs_RED[THEN mp]) |
888 apply(rule abs_RED[THEN mp]) |
889 apply(force dest: fresh_context simp add: psubs_subs) |
889 apply(force dest: fresh_context simp add: psubst_subst) |
890 done |
890 done |