changeset 40888 | 28cd51cff70c |
parent 40774 | 0437dbc127b3 |
child 41036 | 4acbacd6c5bc |
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Dec 01 06:50:54 2010 -0800 +++ b/src/HOL/HOLCF/ConvexPD.thy Wed Dec 01 20:29:39 2010 -0800 @@ -121,7 +121,7 @@ typedef (open) 'a convex_pd = "{S::'a pd_basis set. convex_le.ideal S}" -by (fast intro: convex_le.ideal_principal) +by (rule convex_le.ex_ideal) instantiation convex_pd :: ("domain") below begin