equal
deleted
inserted
replaced
136 using b apply - |
136 using b apply - |
137 apply(erule exE) |
137 apply(erule exE) |
138 apply(rule_tac x="pi \<bullet> pia" in exI) |
138 apply(rule_tac x="pi \<bullet> pia" in exI) |
139 apply(simp add: alpha_gen.simps) |
139 apply(simp add: alpha_gen.simps) |
140 apply(erule conjE)+ |
140 apply(erule conjE)+ |
141 apply(rule conjI)+ |
141 apply(rule conjI) |
142 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
142 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
143 apply(simp add: a[symmetric] atom_eqvt eqvts) |
143 apply(simp add: a[symmetric] atom_eqvt eqvts) |
144 apply(rule conjI) |
144 apply(rule conjI) |
145 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
145 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
146 apply(simp add: a[symmetric] eqvts atom_eqvt) |
146 apply(simp add: a[symmetric] eqvts atom_eqvt) |