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