equal
deleted
inserted
replaced
247 unfolding set_eqvt[symmetric] |
247 unfolding set_eqvt[symmetric] |
248 unfolding supp_eqvt[symmetric] |
248 unfolding supp_eqvt[symmetric] |
249 unfolding Diff_eqvt[symmetric] |
249 unfolding Diff_eqvt[symmetric] |
250 apply(erule_tac [!] exE) |
250 apply(erule_tac [!] exE) |
251 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
251 apply(rule_tac [!] x="p \<bullet> pa" in exI) |
252 by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) |
252 by (auto simp only: fresh_star_permute_iff permute_eqvt[symmetric]) |
253 |
253 |
254 |
254 |
255 section {* Strengthening the equivalence *} |
255 section {* Strengthening the equivalence *} |
256 |
256 |
257 lemma disjoint_right_eq: |
257 lemma disjoint_right_eq: |