| changeset 2987 | 27aab7a105eb |
| parent 2982 | 4a00077c008f |
| child 3026 | b037ae269f50 |
| 2986:847972b7b5ba | 2987:27aab7a105eb |
|---|---|
1013 instantiation "fun" :: (pt, inf_eqvt) inf_eqvt |
1013 instantiation "fun" :: (pt, inf_eqvt) inf_eqvt |
1014 begin |
1014 begin |
1015 |
1015 |
1016 instance |
1016 instance |
1017 apply(default) |
1017 apply(default) |
1018 unfolding Inf_fun_def |
1018 unfolding Inf_fun_def INF_def |
1019 apply(perm_simp) |
1019 apply(perm_simp) |
1020 apply(rule refl) |
1020 apply(rule refl) |
1021 done |
1021 done |
1022 |
1022 |
1023 end |
1023 end |