src/HOLCF/UpperPD.thy
changeset 29244 95d591908d8d
parent 29237 e90d9d51106b
child 29252 ea97aa6aeba2
     1.1 --- a/src/HOLCF/UpperPD.thy	Fri Dec 19 11:09:31 2008 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Fri Dec 19 11:57:21 2008 +0100
     1.3 @@ -248,7 +248,7 @@
     1.4  apply (simp add: PDPlus_absorb)
     1.5  done
     1.6  
     1.7 -interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
     1.8 +class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
     1.9    by unfold_locales
    1.10      (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
    1.11