# HG changeset patch
# User ballarin
# Date 1229684241 -3600
# Node ID 95d591908d8dcb694f698e7c242c1e6aefdadb5a
# Parent  93ef3ae2b9e5cc55120f8fce9f3c22424885e56d
More porting to new locales.

diff -r 93ef3ae2b9e5 -r 95d591908d8d src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -244,7 +244,7 @@
   assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
-  interpret ab_semigroup_idem_mult f by fact
+  class_interpret ab_semigroup_idem_mult [f] by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed
 
diff -r 93ef3ae2b9e5 -r 95d591908d8d src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -296,7 +296,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>"
+class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   by unfold_locales
     (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
 
diff -r 93ef3ae2b9e5 -r 95d591908d8d src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -250,7 +250,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_lower_plus!: ab_semigroup_idem_mult "op +\<flat>"
+class_interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
   by unfold_locales
     (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
 
diff -r 93ef3ae2b9e5 -r 95d591908d8d src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -248,7 +248,7 @@
 apply (simp add: PDPlus_absorb)
 done
 
-interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>"
+class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
   by unfold_locales
     (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+