equal
deleted
inserted
replaced
118 apply(erule exE) |
118 apply(erule exE) |
119 apply(erule conjE) |
119 apply(erule conjE) |
120 apply(rule_tac x="pi \<bullet> pia" in exI) |
120 apply(rule_tac x="pi \<bullet> pia" in exI) |
121 apply(rule conjI) |
121 apply(rule conjI) |
122 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
122 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
123 apply(simp add: eqvts atom_eqvt) |
123 apply(simp only: Diff_eqvt rfv_eqvt insert_eqvt atom_eqvt empty_eqvt) |
|
124 apply(simp) |
124 apply(rule conjI) |
125 apply(rule conjI) |
125 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
126 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
126 apply(simp add: eqvts atom_eqvt) |
127 apply(simp add: Diff_eqvt rfv_eqvt atom_eqvt insert_eqvt empty_eqvt) |
127 apply(subst permute_eqvt[symmetric]) |
128 apply(subst permute_eqvt[symmetric]) |
128 apply(simp) |
129 apply(simp) |
129 done |
130 done |
130 |
131 |
131 lemma alpha_refl: |
132 lemma alpha_refl: |
617 apply(simp add: var_supp1) |
618 apply(simp add: var_supp1) |
618 done |
619 done |
619 |
620 |
620 |
621 |
621 |
622 |
622 end< |
623 end |
623 |
624 |