| changeset 49834 | b27bbb021df1 |
| parent 42151 | 4da4fc77664b |
| child 51489 | f738e6dbd844 |
| 49833:1d80798e8d8a | 49834:b27bbb021df1 |
|---|---|
72 done |
72 done |
73 |
73 |
74 |
74 |
75 subsection {* Type definition *} |
75 subsection {* Type definition *} |
76 |
76 |
77 typedef (open) 'a lower_pd = |
77 typedef 'a lower_pd = |
78 "{S::'a pd_basis set. lower_le.ideal S}" |
78 "{S::'a pd_basis set. lower_le.ideal S}" |
79 by (rule lower_le.ex_ideal) |
79 by (rule lower_le.ex_ideal) |
80 |
80 |
81 type_notation (xsymbols) lower_pd ("('(_')\<flat>)") |
81 type_notation (xsymbols) lower_pd ("('(_')\<flat>)") |
82 |
82 |