changeset 49834 | b27bbb021df1 |
parent 45606 | b1e1508643b1 |
child 51489 | f738e6dbd844 |
--- a/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 18:58:20 2012 +0200 @@ -119,7 +119,7 @@ subsection {* Type definition *} -typedef (open) 'a convex_pd = +typedef 'a convex_pd = "{S::'a pd_basis set. convex_le.ideal S}" by (rule convex_le.ex_ideal)