equal
deleted
inserted
replaced
108 apply(rule conjI) |
108 apply(rule conjI) |
109 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
109 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
110 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
110 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
111 apply(subst permute_eqvt[symmetric]) |
111 apply(subst permute_eqvt[symmetric]) |
112 apply(simp) |
112 apply(simp) |
113 oops |
113 apply(simp add: c[symmetric]) |
|
114 apply(subst permute_eqvt[symmetric]) |
|
115 apply simp |
|
116 done |
114 |
117 |
115 fun |
118 fun |
116 alpha_abs |
119 alpha_abs |
117 where |
120 where |
118 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
121 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |