equal
deleted
inserted
replaced
73 subsection {* Type definition *} |
73 subsection {* Type definition *} |
74 |
74 |
75 typedef (open) 'a upper_pd = |
75 typedef (open) 'a upper_pd = |
76 "{S::'a pd_basis set. upper_le.ideal S}" |
76 "{S::'a pd_basis set. upper_le.ideal S}" |
77 by (rule upper_le.ex_ideal) |
77 by (rule upper_le.ex_ideal) |
|
78 |
|
79 type_notation (xsymbols) upper_pd ("('(_')\<sharp>)") |
78 |
80 |
79 instantiation upper_pd :: ("domain") below |
81 instantiation upper_pd :: ("domain") below |
80 begin |
82 begin |
81 |
83 |
82 definition |
84 definition |