equal
deleted
inserted
replaced
208 |
208 |
209 lemma ty_of_permute [simp]: |
209 lemma ty_of_permute [simp]: |
210 shows "ty_of (p \<bullet> x) = ty_of x" |
210 shows "ty_of (p \<bullet> x) = ty_of x" |
211 unfolding ty_of_def |
211 unfolding ty_of_def |
212 unfolding atom_eqvt [symmetric] |
212 unfolding atom_eqvt [symmetric] |
213 by simp |
213 by (simp only: sort_of_permute) |
214 |
214 |
215 |
215 |
216 section {* Tests with subtyping and automatic coercions *} |
216 section {* Tests with subtyping and automatic coercions *} |
217 |
217 |
218 declare [[coercion_enabled]] |
218 declare [[coercion_enabled]] |
234 coercion map *) |
234 coercion map *) |
235 |
235 |
236 lemma |
236 lemma |
237 fixes as::"var1 set" |
237 fixes as::"var1 set" |
238 shows "atom ` as \<sharp>* t" |
238 shows "atom ` as \<sharp>* t" |
|
239 |
239 oops |
240 oops |
240 |
241 |
241 end |
242 end |