| changeset 3245 | 017e33849f4d |
| parent 3065 | 51ef8a3cb6ef |
| 3244:a44479bde681 | 3245:017e33849f4d |
|---|---|
42 |
42 |
43 definition |
43 definition |
44 "p \<bullet> (f::foo) = f" |
44 "p \<bullet> (f::foo) = f" |
45 |
45 |
46 instance |
46 instance |
47 apply(default) |
47 apply(standard) |
48 apply(simp_all add: permute_foo_def) |
48 apply(simp_all add: permute_foo_def) |
49 done |
49 done |
50 |
50 |
51 end |
51 end |
52 |
52 |