| changeset 2524 | 693562f03eee |
| parent 2509 | 679cef364022 |
| child 2559 | add799cf0817 |
| 2523:e903c32ec24f | 2524:693562f03eee |
|---|---|
155 apply(rule at_set_avoiding2) |
155 apply(rule at_set_avoiding2) |
156 apply(simp add: finite_supp) |
156 apply(simp add: finite_supp) |
157 apply(simp add: finite_supp) |
157 apply(simp add: finite_supp) |
158 apply(simp add: finite_supp) |
158 apply(simp add: finite_supp) |
159 oops |
159 oops |
160 (*apply(simp add: Abs_fresh_star)*) |
160 |
161 sorry |
|
162 |
|
163 done |
|
164 |
161 |
165 end |
162 end |
166 |
163 |
167 |
164 |
168 |
165 |