equal
deleted
inserted
replaced
236 apply (case_tac x) |
236 apply (case_tac x) |
237 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
237 apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1)) |
238 apply (auto simp add: fresh_star_def)[3] |
238 apply (auto simp add: fresh_star_def)[3] |
239 apply (drule_tac x="assn" in meta_spec) |
239 apply (drule_tac x="assn" in meta_spec) |
240 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
240 apply (simp add: Abs1_eq_iff alpha_bn_refl) |
241 apply auto |
241 apply auto[7] |
|
242 prefer 2 |
|
243 apply(simp) |
|
244 thm subst_sumC_def |
|
245 thm THE_default_def |
|
246 thm theI |
242 apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) |
247 apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2) |
243 apply (simp add: Abs_fresh_iff) |
248 apply (simp add: Abs_fresh_iff) |
244 apply (simp add: fresh_star_def) |
249 apply (simp add: fresh_star_def) |
245 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2] |
250 apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2] |
246 apply (subgoal_tac "apply_assn2 (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2)) asa |
251 apply (subgoal_tac "apply_assn2 (\<lambda>x2\<Colon>trm. subst_sumC (sa, ta, x2)) asa |