equal
deleted
inserted
replaced
607 apply (induct ys rule: convex_pd.principal_induct, simp) |
607 apply (induct ys rule: convex_pd.principal_induct, simp) |
608 apply (simp add: convex_le_def) |
608 apply (simp add: convex_le_def) |
609 done |
609 done |
610 |
610 |
611 lemmas convex_plus_below_plus_iff = |
611 lemmas convex_plus_below_plus_iff = |
612 convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard] |
612 convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws"] |
|
613 for xs ys zs ws |
613 |
614 |
614 lemmas convex_pd_below_simps = |
615 lemmas convex_pd_below_simps = |
615 convex_unit_below_plus_iff |
616 convex_unit_below_plus_iff |
616 convex_plus_below_unit_iff |
617 convex_plus_below_unit_iff |
617 convex_plus_below_plus_iff |
618 convex_plus_below_plus_iff |