| changeset 45606 | b1e1508643b1 |
| parent 42151 | 4da4fc77664b |
| child 49834 | b27bbb021df1 |
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Nov 20 21:05:23 2011 +0100 +++ b/src/HOL/HOLCF/ConvexPD.thy Sun Nov 20 21:07:06 2011 +0100 @@ -609,7 +609,8 @@ done lemmas convex_plus_below_plus_iff = - convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard] + convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"] + for xs ys zs ws lemmas convex_pd_below_simps = convex_unit_below_plus_iff