# HG changeset patch
# User wenzelm
# Date 1447080497 -3600
# Node ID 1bf7b186542e0c34b0afa3e30f578d253b90c88f
# Parent  bb20f11dd842e9c45042de7f2e83b16170cf8f3c
qualifier is mandatory by default;

diff -r bb20f11dd842 -r 1bf7b186542e src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -775,7 +775,7 @@
 
 locale container
 begin
-interpretation "private"!: roundup True by unfold_locales rule
+interpretation "private": roundup True by unfold_locales rule
 lemmas true_copy = private.true
 end
 
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Algebra/Ring.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -94,7 +94,7 @@
 text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
 
 sublocale abelian_monoid <
-  add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  add: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
@@ -112,7 +112,7 @@
 end
 
 sublocale abelian_monoid <
-  add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  add: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
@@ -168,7 +168,7 @@
 end
 
 sublocale abelian_group <
-  add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  add: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
@@ -196,7 +196,7 @@
 end
 
 sublocale abelian_group <
-  add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  add: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
     and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
     and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -498,8 +498,8 @@
   and     sWELL: "Well_order s"
 begin
 
-interpretation r!: wo_rel r by unfold_locales (rule rWELL)
-interpretation s!: wo_rel s by unfold_locales (rule sWELL)
+interpretation r: wo_rel r by unfold_locales (rule rWELL)
+interpretation s: wo_rel s by unfold_locales (rule sWELL)
 
 abbreviation "SUPP \<equiv> support r.zero (Field s)"
 abbreviation "FINFUNC \<equiv> FinFunc r s"
@@ -1134,8 +1134,8 @@
   moreover
   from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce
   moreover
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
     unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
     by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
@@ -1200,8 +1200,8 @@
   from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
     by auto (metis well_order_on_domain t, metis well_order_on_domain s)
   moreover
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
     unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
     by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
@@ -1277,12 +1277,12 @@
   assumes "oone <o r" "s <o t"
   shows   "r ^o s <o r ^o t" (is "?L <o ?R")
 proof -
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
-  interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret rexpt: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
   have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
   moreover
   { assume "Field r = {r.zero}"
@@ -1388,11 +1388,11 @@
   assumes "r \<le>o s"
   shows   "r ^o t \<le>o s ^o t"
 proof -
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
-  interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret st: wo_rel2 s t by unfold_locales (rule s, rule t)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
   show ?thesis
   proof (cases "t = {}")
     case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
@@ -1453,9 +1453,9 @@
   assumes "oone <o r"
   shows   "s \<le>o r ^o s"
 proof -
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
   from assms well_order_on_domain[OF r] obtain x where
     x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
     unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
@@ -1511,9 +1511,9 @@
     "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
   shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
 proof -
-  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inl x)"
     using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
   hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
@@ -1535,9 +1535,9 @@
     "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
   shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
 proof -
-  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inr x)"
     using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
   hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
@@ -1548,9 +1548,9 @@
 
 lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
 proof (rule ordIso_symmetric)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
   let ?f = "\<lambda>(f, g). case_sum f g"
   have "bij_betw ?f (Field ?L) (Field ?R)"
   unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
@@ -1581,8 +1581,8 @@
   assumes Field: "Field r \<noteq> {}"
   shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
 proof safe
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   fix g assume g: "g \<in> FinFunc r (s *o t)"
   hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))"
     unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
@@ -1591,8 +1591,8 @@
     unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
     by (auto simp: rev_curr_def fin_support_def)
 next
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   fix fg assume *: "fg \<in> FinFunc (r ^o s) t"
   let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined"
   show "fg \<in> rev_curr ` FinFunc r (s *o t)"
@@ -1631,12 +1631,12 @@
   shows "wo_rel.max_fun_diff (s *o t) f g =
     (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
 proof -
-  interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret st: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
     have diff1: "rev_curr f \<noteq> rev_curr g"
       "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
@@ -1668,8 +1668,8 @@
 lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
 proof (cases "r = {}")
   case True
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   show ?thesis
   proof (cases "s = {} \<or> t = {}")
     case True with `r = {}` show ?thesis
@@ -1687,9 +1687,9 @@
   hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty)
   show ?thesis
   proof (rule ordIso_symmetric)
-    interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
-    interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-    interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+    interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+    interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+    interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
     have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
     unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
       show "inj_on rev_curr (FinFunc r (s *o t))"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -932,8 +932,8 @@
 and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
 shows "\<exists> g. embed r s g"
 proof-
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
   let ?G = "\<lambda> g a. suc s (g ` underS r a)"
   def g \<equiv> "worec r ?G"
   have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -1196,12 +1196,12 @@
 definition card :: "'a set \<Rightarrow> nat" where
   "card = folding.F (\<lambda>_. Suc) 0"
 
-interpretation card!: folding "\<lambda>_. Suc" 0
+interpretation card: folding "\<lambda>_. Suc" 0
 rewrites
   "folding.F (\<lambda>_. Suc) 0 = card"
 proof -
   show "folding (\<lambda>_. Suc)" by standard rule
-  then interpret card!: folding "\<lambda>_. Suc" 0 .
+  then interpret card: folding "\<lambda>_. Suc" 0 .
   from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
 qed
 
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/GCD.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -104,7 +104,7 @@
   "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
 
-sublocale gcd!: abel_semigroup gcd
+sublocale gcd: abel_semigroup gcd
 proof
   fix a b c
   show "gcd a b = gcd b a"
@@ -256,7 +256,7 @@
   "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
 
-sublocale lcm!: abel_semigroup lcm
+sublocale lcm: abel_semigroup lcm
 proof
   fix a b c
   show "lcm a b = lcm b a"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Groups.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -131,7 +131,7 @@
   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
 begin
 
-sublocale add!: semigroup plus
+sublocale add: semigroup plus
   by standard (fact add_assoc)
 
 end
@@ -142,7 +142,7 @@
   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
 begin
 
-sublocale add!: abel_semigroup plus
+sublocale add: abel_semigroup plus
   by standard (fact add_commute)
 
 declare add.left_commute [algebra_simps, field_simps]
@@ -159,7 +159,7 @@
   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
 begin
 
-sublocale mult!: semigroup times
+sublocale mult: semigroup times
   by standard (fact mult_assoc)
 
 end
@@ -170,7 +170,7 @@
   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
 begin
 
-sublocale mult!: abel_semigroup times
+sublocale mult: abel_semigroup times
   by standard (fact mult_commute)
 
 declare mult.left_commute [algebra_simps, field_simps]
@@ -188,7 +188,7 @@
     and add_0_right: "a + 0 = a"
 begin
 
-sublocale add!: monoid plus 0
+sublocale add: monoid plus 0
   by standard (fact add_0_left add_0_right)+
 
 end
@@ -203,7 +203,7 @@
 subclass monoid_add
   by standard (simp_all add: add_0 add.commute [of _ 0])
 
-sublocale add!: comm_monoid plus 0
+sublocale add: comm_monoid plus 0
   by standard (simp add: ac_simps)
 
 end
@@ -213,7 +213,7 @@
     and mult_1_right: "a * 1 = a"
 begin
 
-sublocale mult!: monoid times 1
+sublocale mult: monoid times 1
   by standard (fact mult_1_left mult_1_right)+
 
 end
@@ -228,7 +228,7 @@
 subclass monoid_mult
   by standard (simp_all add: mult_1 mult.commute [of _ 1])
 
-sublocale mult!: comm_monoid times 1
+sublocale mult: comm_monoid times 1
   by standard (simp add: ac_simps)
 
 end
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -471,12 +471,12 @@
 where
   "setsum = comm_monoid_set.F plus 0"
 
-sublocale setsum!: comm_monoid_set plus 0
+sublocale setsum: comm_monoid_set plus 0
 rewrites
   "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_set plus 0" ..
-  then interpret setsum!: comm_monoid_set plus 0 .
+  then interpret setsum: comm_monoid_set plus 0 .
   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
 qed
 
@@ -1062,12 +1062,12 @@
 where
   "setprod = comm_monoid_set.F times 1"
 
-sublocale setprod!: comm_monoid_set times 1
+sublocale setprod: comm_monoid_set times 1
 rewrites
   "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_set times 1" ..
-  then interpret setprod!: comm_monoid_set times 1 .
+  then interpret setprod: comm_monoid_set times 1 .
   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
 qed
 
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Groups_List.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -65,12 +65,12 @@
 where
   "listsum  = monoid_list.F plus 0"
 
-sublocale listsum!: monoid_list plus 0
+sublocale listsum: monoid_list plus 0
 rewrites
  "monoid_list.F plus 0 = listsum"
 proof -
   show "monoid_list plus 0" ..
-  then interpret listsum!: monoid_list plus 0 .
+  then interpret listsum: monoid_list plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
 qed
  
@@ -79,22 +79,22 @@
 context comm_monoid_add
 begin
 
-sublocale listsum!: comm_monoid_list plus 0
+sublocale listsum: comm_monoid_list plus 0
 rewrites
   "monoid_list.F plus 0 = listsum"
 proof -
   show "comm_monoid_list plus 0" ..
-  then interpret listsum!: comm_monoid_list plus 0 .
+  then interpret listsum: comm_monoid_list plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
 qed
 
-sublocale setsum!: comm_monoid_list_set plus 0
+sublocale setsum: comm_monoid_list_set plus 0
 rewrites
   "monoid_list.F plus 0 = listsum"
   and "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_list_set plus 0" ..
-  then interpret setsum!: comm_monoid_list_set plus 0 .
+  then interpret setsum: comm_monoid_list_set plus 0 .
   from listsum_def show "monoid_list.F plus 0 = listsum" by rule
   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
 qed
@@ -332,12 +332,12 @@
 where
   "listprod  = monoid_list.F times 1"
 
-sublocale listprod!: monoid_list times 1
+sublocale listprod: monoid_list times 1
 rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "monoid_list times 1" ..
-  then interpret listprod!: monoid_list times 1 .
+  then interpret listprod: monoid_list times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
 qed
 
@@ -346,22 +346,22 @@
 context comm_monoid_mult
 begin
 
-sublocale listprod!: comm_monoid_list times 1
+sublocale listprod: comm_monoid_list times 1
 rewrites
   "monoid_list.F times 1 = listprod"
 proof -
   show "comm_monoid_list times 1" ..
-  then interpret listprod!: comm_monoid_list times 1 .
+  then interpret listprod: comm_monoid_list times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
 qed
 
-sublocale setprod!: comm_monoid_list_set times 1
+sublocale setprod: comm_monoid_list_set times 1
 rewrites
   "monoid_list.F times 1 = listprod"
   and "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_list_set times 1" ..
-  then interpret setprod!: comm_monoid_list_set times 1 .
+  then interpret setprod: comm_monoid_list_set times 1 .
   from listprod_def show "monoid_list.F times 1 = listprod" by rule
   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
 qed
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -836,7 +836,7 @@
 
 end
 
-interpretation compact_basis!:
+interpretation compact_basis:
   ideal_completion below Rep_compact_basis
     "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
 proof -
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -404,7 +404,7 @@
     by (simp only: Heap_ord_def Heap_lub_def)
 qed
 
-interpretation heap!: partial_function_definitions Heap_ord Heap_lub
+interpretation heap: partial_function_definitions Heap_ord Heap_lub
   rewrites "Heap_lub {} \<equiv> Heap Map.empty"
 by (fact heap_interpretation)(simp add: Heap_lub_empty)
 
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Lattices.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -271,7 +271,7 @@
 context semilattice_inf
 begin
 
-sublocale inf!: semilattice inf
+sublocale inf: semilattice inf
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -282,7 +282,7 @@
     by (rule antisym) (auto simp add: le_inf_iff)
 qed
 
-sublocale inf!: semilattice_order inf less_eq less
+sublocale inf: semilattice_order inf less_eq less
   by standard (auto simp add: le_iff_inf less_le)
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
@@ -316,7 +316,7 @@
 context semilattice_sup
 begin
 
-sublocale sup!: semilattice sup
+sublocale sup: semilattice sup
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
@@ -327,7 +327,7 @@
     by (rule antisym) (auto simp add: le_sup_iff)
 qed
 
-sublocale sup!: semilattice_order sup greater_eq greater
+sublocale sup: semilattice_order sup greater_eq greater
   by standard (auto simp add: le_iff_sup sup.commute less_le)
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
@@ -484,8 +484,8 @@
 class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
 
-sublocale inf_top!: semilattice_neutr inf top
-  + inf_top!: semilattice_neutr_order inf top less_eq less
+sublocale inf_top: semilattice_neutr inf top
+  + inf_top: semilattice_neutr_order inf top less_eq less
 proof
   fix x
   show "x \<sqinter> \<top> = x"
@@ -497,8 +497,8 @@
 class bounded_semilattice_sup_bot = semilattice_sup + order_bot
 begin
 
-sublocale sup_bot!: semilattice_neutr sup bot
-  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
+sublocale sup_bot: semilattice_neutr sup bot
+  + sup_bot: semilattice_neutr_order sup bot greater_eq greater
 proof
   fix x
   show "x \<squnion> \<bottom> = x"
@@ -715,8 +715,8 @@
 context linorder
 begin
 
-sublocale min!: semilattice_order min less_eq less
-  + max!: semilattice_order max greater_eq greater
+sublocale min: semilattice_order min less_eq less
+  + max: semilattice_order max greater_eq greater
   by standard (auto simp add: min_def max_def)
 
 lemma min_le_iff_disj:
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Lattices_Big.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -318,12 +318,12 @@
 where
   "Inf_fin = semilattice_set.F inf"
 
-sublocale Inf_fin!: semilattice_order_set inf less_eq less
+sublocale Inf_fin: semilattice_order_set inf less_eq less
 rewrites
   "semilattice_set.F inf = Inf_fin"
 proof -
   show "semilattice_order_set inf less_eq less" ..
-  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
+  then interpret Inf_fin: semilattice_order_set inf less_eq less .
   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
 qed
 
@@ -336,12 +336,12 @@
 where
   "Sup_fin = semilattice_set.F sup"
 
-sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
+sublocale Sup_fin: semilattice_order_set sup greater_eq greater
 rewrites
   "semilattice_set.F sup = Sup_fin"
 proof -
   show "semilattice_order_set sup greater_eq greater" ..
-  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
+  then interpret Sup_fin: semilattice_order_set sup greater_eq greater .
   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
 qed
 
@@ -490,16 +490,16 @@
 where
   "Max = semilattice_set.F max"
 
-sublocale Min!: semilattice_order_set min less_eq less
-  + Max!: semilattice_order_set max greater_eq greater
+sublocale Min: semilattice_order_set min less_eq less
+  + Max: semilattice_order_set max greater_eq greater
 rewrites
   "semilattice_set.F min = Min"
   and "semilattice_set.F max = Max"
 proof -
   show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
-  then interpret Min!: semilattice_order_set min less_eq less .
+  then interpret Min: semilattice_order_set min less_eq less .
   show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
-  then interpret Max!: semilattice_order_set max greater_eq greater .
+  then interpret Max: semilattice_order_set max greater_eq greater .
   from Min_def show "semilattice_set.F min = Min" by rule
   from Max_def show "semilattice_set.F max = Max" by rule
 qed
@@ -530,14 +530,14 @@
 lemma dual_Min:
   "linorder.Min greater_eq = Max"
 proof -
-  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
+  interpret dual: linorder greater_eq greater by (fact dual_linorder)
   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
 qed
 
 lemma dual_Max:
   "linorder.Max greater_eq = Min"
 proof -
-  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
+  interpret dual: linorder greater_eq greater by (fact dual_linorder)
   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
 qed
 
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -26,10 +26,10 @@
   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
 begin
 
-sublocale conj!: abel_semigroup conj
+sublocale conj: abel_semigroup conj
   by standard (fact conj_assoc conj_commute)+
 
-sublocale disj!: abel_semigroup disj
+sublocale disj: abel_semigroup disj
   by standard (fact disj_assoc disj_commute)+
 
 lemmas conj_left_commute = conj.left_commute
@@ -190,7 +190,7 @@
   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
 begin
 
-sublocale xor!: abel_semigroup xor
+sublocale xor: abel_semigroup xor
 proof
   fix x y z :: 'a
   let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -20,7 +20,7 @@
 where
   expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
 
-interpretation F!: comm_monoid_set f 1
+interpretation F: comm_monoid_set f 1
   ..
 
 lemma expand_superset:
@@ -225,13 +225,13 @@
 where
   "Sum_any = comm_monoid_fun.G plus 0"
 
-permanent_interpretation Sum_any!: comm_monoid_fun plus 0
+permanent_interpretation Sum_any: comm_monoid_fun plus 0
 where
   "comm_monoid_fun.G plus 0 = Sum_any" and
   "comm_monoid_set.F plus 0 = setsum"
 proof -
   show "comm_monoid_fun plus 0" ..
-  then interpret Sum_any!: comm_monoid_fun plus 0 .
+  then interpret Sum_any: comm_monoid_fun plus 0 .
   from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
 qed
@@ -298,13 +298,13 @@
 where
   "Prod_any = comm_monoid_fun.G times 1"
 
-permanent_interpretation Prod_any!: comm_monoid_fun times 1
+permanent_interpretation Prod_any: comm_monoid_fun times 1
 where
   "comm_monoid_fun.G times 1 = Prod_any" and
   "comm_monoid_set.F times 1 = setprod"
 proof -
   show "comm_monoid_fun times 1" ..
-  then interpret Prod_any!: comm_monoid_fun times 1 .
+  then interpret Prod_any: comm_monoid_fun times 1 .
   from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
 qed
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -1058,7 +1058,7 @@
 where
   "mset_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
 
-interpretation mset_set!: folding "\<lambda>x M. {#x#} + M" "{#}"
+interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
 rewrites
   "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
 proof -
@@ -1221,7 +1221,7 @@
 definition msetsum :: "'a multiset \<Rightarrow> 'a"
   where "msetsum = comm_monoid_mset.F plus 0"
 
-sublocale msetsum!: comm_monoid_mset plus 0
+sublocale msetsum: comm_monoid_mset plus 0
   rewrites "comm_monoid_mset.F plus 0 = msetsum"
 proof -
   show "comm_monoid_mset plus 0" ..
@@ -1279,7 +1279,7 @@
 definition msetprod :: "'a multiset \<Rightarrow> 'a"
   where "msetprod = comm_monoid_mset.F times 1"
 
-sublocale msetprod!: comm_monoid_mset times 1
+sublocale msetprod: comm_monoid_mset times 1
   rewrites "comm_monoid_mset.F times 1 = msetprod"
 proof -
   show "comm_monoid_mset times 1" ..
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -1887,7 +1887,7 @@
     by (rule poly_dvd_antisym)
 qed
 
-interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
+interpretation gcd_poly: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
 proof
   fix x y z :: "'a poly"
   show "gcd (gcd x y) z = gcd x (gcd y z)"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Library/Saturated.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -214,7 +214,7 @@
 
 end
 
-interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
+interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
 rewrites
   "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
@@ -224,7 +224,7 @@
     by (simp add: Inf_sat_def)
 qed
 
-interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
+interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
 rewrites
   "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/List.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -5150,7 +5150,7 @@
 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   "sorted_list_of_set = folding.F insort []"
 
-sublocale sorted_list_of_set!: folding insort Nil
+sublocale sorted_list_of_set: folding insort Nil
 rewrites
   "folding.F insort [] = sorted_list_of_set"
 proof -
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -238,7 +238,7 @@
   shows "c = gcd a b"
   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
 
-sublocale gcd!: abel_semigroup gcd
+sublocale gcd: abel_semigroup gcd
 proof
   fix a b c 
   show "gcd (gcd a b) c = gcd a (gcd b c)"
@@ -790,7 +790,7 @@
   shows "c = lcm a b"
   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
 
-sublocale lcm!: abel_semigroup lcm ..
+sublocale lcm: abel_semigroup lcm ..
 
 lemma dvd_lcm_D1:
   "lcm m n dvd k \<Longrightarrow> m dvd k"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Orderings.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -191,7 +191,7 @@
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   by (auto simp add: less_le_not_le intro: antisym)
 
-sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
+sublocale order: ordering less_eq less +  dual_order: ordering greater_eq greater
   by standard (auto intro: antisym order_trans simp add: less_le)
 
 
@@ -1181,7 +1181,7 @@
   assumes bot_least: "\<bottom> \<le> a"
 begin
 
-sublocale bot!: ordering_top greater_eq greater bot
+sublocale bot: ordering_top greater_eq greater bot
   by standard (fact bot_least)
 
 lemma le_bot:
@@ -1209,7 +1209,7 @@
   assumes top_greatest: "a \<le> \<top>"
 begin
 
-sublocale top!: ordering_top less_eq less top
+sublocale top: ordering_top less_eq less top
   by standard (fact top_greatest)
 
 lemma top_le:
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Partial_Function.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -281,12 +281,12 @@
 lemma antisymP_flat_ord: "antisymP (flat_ord a)"
 by(rule antisymI)(auto dest: flat_ord_antisym)
 
-interpretation tailrec!:
+interpretation tailrec:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   rewrites "flat_lub undefined {} \<equiv> undefined"
 by (rule flat_interpretation)(simp add: flat_lub_def)
 
-interpretation option!:
+interpretation option:
   partial_function_definitions "flat_ord None" "flat_lub None"
   rewrites "flat_lub None {} \<equiv> None"
 by (rule flat_interpretation)(simp add: flat_lub_def)
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -709,7 +709,7 @@
 lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
   by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ereal_def[symmetric])
 
-interpretation lborel!: sigma_finite_measure lborel
+interpretation lborel: sigma_finite_measure lborel
   by (rule sigma_finite_lborel)
 
 interpretation lborel_pair: pair_sigma_finite lborel lborel ..
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -113,10 +113,10 @@
 lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
   using pmf.measure_pmf[of p] by auto
 
-interpretation measure_pmf!: prob_space "measure_pmf M" for M
+interpretation measure_pmf: prob_space "measure_pmf M" for M
   by (rule prob_space_measure_pmf)
 
-interpretation measure_pmf!: subprob_space "measure_pmf M" for M
+interpretation measure_pmf: subprob_space "measure_pmf M" for M
   by (rule prob_space_imp_subprob_space) unfold_locales
 
 lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -46,7 +46,7 @@
 lemma prob_space_distrD:
   assumes f: "f \<in> measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
 proof
-  interpret M!: prob_space "distr M N f" by fact
+  interpret M: prob_space "distr M N f" by fact
   have "f -` space N \<inter> space M = space M"
     using f[THEN measurable_space] by auto
   then show "emeasure M (space M) = 1"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -97,7 +97,7 @@
     by simp
 qed (force simp: generator.simps prod_emb_empty[symmetric])
 
-interpretation generator!: algebra "space (PiM I M)" generator
+interpretation generator: algebra "space (PiM I M)" generator
   by (rule algebra_generator)
 
 lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
@@ -407,7 +407,7 @@
 definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
 
-sublocale PF!: projective_family UNIV CI
+sublocale PF: projective_family UNIV CI
   unfolding projective_family_def
 proof safe
   show "finite J \<Longrightarrow> prob_space (CI J)" for J
@@ -460,7 +460,7 @@
   also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
   proof (intro INF_greatest)
     fix n
-    interpret C!: prob_space "C 0 n (\<lambda>x. undefined)"
+    interpret C: prob_space "C 0 n (\<lambda>x. undefined)"
       by (rule prob_space_C) simp
     show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
     proof cases
@@ -606,9 +606,9 @@
       using count by (auto simp: t_def)
     then have inj_t_J: "inj_on t (J i)" for i
       by (rule subset_inj_on) auto
-    interpret IT!: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
+    interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
       by standard auto
-    interpret Mf!: product_prob_space "\<lambda>x. M (f x)" UNIV
+    interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
       by standard
     have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
     proof (induction n)
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -469,7 +469,7 @@
 hide_const (open) domain
 hide_const (open) basis_finmap
 
-sublocale polish_projective \<subseteq> P!: prob_space lim
+sublocale polish_projective \<subseteq> P: prob_space lim
 proof
   have *: "emb I {} {\<lambda>x. undefined} = space (\<Pi>\<^sub>M i\<in>I. borel)"
     by (auto simp: prod_emb_def space_PiM)
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -935,7 +935,7 @@
     by (auto intro: density_cong)
 next
   assume eq: "density M f = density M g"
-  interpret f!: sigma_finite_measure "density M f" by fact
+  interpret f: sigma_finite_measure "density M f" by fact
   from f.sigma_finite_incseq guess A . note cover = this
 
   have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -1479,7 +1479,7 @@
 lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
   by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
 
-interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
+interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
   using measure_space[of M] by (auto simp: measure_space_def)
 
 definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where