src/HOLCF/LowerPD.thy

--- a/src/HOLCF/LowerPD.thy	Mon Feb 04 17:00:01 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Wed Feb 06 08:34:32 2008 +0100
@@ -433,10 +433,10 @@
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
     (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 
-lemma ACI_lower_bind: "ACIf (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
 apply unfold_locales
+apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
-apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_absorb eta_cfun)
 done
 
@@ -447,8 +447,8 @@
     (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
 unfolding lower_bind_basis_def
 apply -
-apply (rule ACIf.fold_pd_PDUnit [OF ACI_lower_bind])
-apply (rule ACIf.fold_pd_PDPlus [OF ACI_lower_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
+apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
 done
 
 lemma lower_bind_basis_mono: