More porting to new locales.
authorballarin
Fri Dec 19 11:57:21 2008 +0100 (2008-12-19)
changeset 2924495d591908d8d
parent 29243 93ef3ae2b9e5
child 29245 19728ee2b1ba
More porting to new locales.
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:09:31 2008 +0100
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:57:21 2008 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4    assumes "ab_semigroup_idem_mult f"
     1.5    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
     1.6  proof -
     1.7 -  interpret ab_semigroup_idem_mult f by fact
     1.8 +  class_interpret ab_semigroup_idem_mult [f] by fact
     1.9    show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
    1.10  qed
    1.11  
     2.1 --- a/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:09:31 2008 +0100
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:57:21 2008 +0100
     2.3 @@ -296,7 +296,7 @@
     2.4  apply (simp add: PDPlus_absorb)
     2.5  done
     2.6  
     2.7 -interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
     2.8 +class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
     2.9    by unfold_locales
    2.10      (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
    2.11  
     3.1 --- a/src/HOLCF/LowerPD.thy	Fri Dec 19 11:09:31 2008 +0100
     3.2 +++ b/src/HOLCF/LowerPD.thy	Fri Dec 19 11:57:21 2008 +0100
     3.3 @@ -250,7 +250,7 @@
     3.4  apply (simp add: PDPlus_absorb)
     3.5  done
     3.6  
     3.7 -interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
     3.8 +class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
     3.9    by unfold_locales
    3.10      (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
    3.11  
     4.1 --- a/src/HOLCF/UpperPD.thy	Fri Dec 19 11:09:31 2008 +0100
     4.2 +++ b/src/HOLCF/UpperPD.thy	Fri Dec 19 11:57:21 2008 +0100
     4.3 @@ -248,7 +248,7 @@
     4.4  apply (simp add: PDPlus_absorb)
     4.5  done
     4.6  
     4.7 -interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
     4.8 +class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
     4.9    by unfold_locales
    4.10      (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
    4.11