1.1 --- a/src/HOLCF/ConvexPD.thy	Mon Feb 04 17:00:01 2008 +0100
     1.2 +++ b/src/HOLCF/ConvexPD.thy	Wed Feb 06 08:34:32 2008 +0100
     1.3 @@ -443,10 +443,10 @@
     1.4      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     1.5      (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.6  
     1.7 -lemma ACI_convex_bind: "ACIf (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.8 +lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
     1.9  apply unfold_locales
    1.10 +apply (simp add: convex_plus_assoc)
    1.11  apply (simp add: convex_plus_commute)
    1.12 -apply (simp add: convex_plus_assoc)
    1.13  apply (simp add: convex_plus_absorb eta_cfun)
    1.14  done
    1.15  
    1.16 @@ -457,8 +457,8 @@
    1.17      (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
    1.18  unfolding convex_bind_basis_def
    1.19  apply -
    1.20 -apply (rule ACIf.fold_pd_PDUnit [OF ACI_convex_bind])
    1.21 -apply (rule ACIf.fold_pd_PDPlus [OF ACI_convex_bind])
    1.22 +apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
    1.23 +apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
    1.24  done
    1.25  
    1.26  lemma monofun_LAM: