src/HOLCF/ConvexPD.thy

 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
 by (rule aci_convex_plus.mult_left_commute)
 
 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
 by (rule aci_convex_plus.mult_left_idem)
-
+(*
 lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
-
+*)
 lemma convex_unit_less_plus_iff [simp]:
   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")