equal
deleted
inserted
replaced
75 subsection {* Type definition *} |
75 subsection {* Type definition *} |
76 |
76 |
77 typedef (open) 'a lower_pd = |
77 typedef (open) '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 |
|
81 type_notation (xsymbols) lower_pd ("('(_')\<flat>)") |
80 |
82 |
81 instantiation lower_pd :: ("domain") below |
83 instantiation lower_pd :: ("domain") below |
82 begin |
84 begin |
83 |
85 |
84 definition |
86 definition |