changeset 3183 | 313e6f2cdd89 |
parent 2891 | 304dfe6cc83a |
child 3202 | 3611bc56c177 |
--- a/Nominal/Atoms.thy Thu May 31 12:01:13 2012 +0100 +++ b/Nominal/Atoms.thy Mon Jun 04 21:39:51 2012 +0100 @@ -210,7 +210,7 @@ shows "ty_of (p \<bullet> x) = ty_of x" unfolding ty_of_def unfolding atom_eqvt [symmetric] - by simp + by (simp only: sort_of_permute) section {* Tests with subtyping and automatic coercions *} @@ -236,6 +236,7 @@ lemma fixes as::"var1 set" shows "atom ` as \<sharp>* t" + oops end