equal
deleted
inserted
replaced
119 |
119 |
120 subsection {* Type definition *} |
120 subsection {* Type definition *} |
121 |
121 |
122 typedef (open) 'a convex_pd = |
122 typedef (open) 'a convex_pd = |
123 "{S::'a pd_basis set. convex_le.ideal S}" |
123 "{S::'a pd_basis set. convex_le.ideal S}" |
124 by (fast intro: convex_le.ideal_principal) |
124 by (rule convex_le.ex_ideal) |
125 |
125 |
126 instantiation convex_pd :: ("domain") below |
126 instantiation convex_pd :: ("domain") below |
127 begin |
127 begin |
128 |
128 |
129 definition |
129 definition |