qualifier is mandatory by default;
authorwenzelm
Mon Nov 09 15:48:17 2015 +0100 (2015-11-09)
changeset 616051bf7b186542e
parent 61604 bb20f11dd842
child 61606 6d5213bd9709
qualifier is mandatory by default;
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/HOL/Algebra/Ring.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Cardinals/Wellorder_Constructions.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Groups_List.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Lattices.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Saturated.thy
src/HOL/List.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Orderings.thy
src/HOL/Partial_Function.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -775,7 +775,7 @@
     1.4  
     1.5  locale container
     1.6  begin
     1.7 -interpretation "private"!: roundup True by unfold_locales rule
     1.8 +interpretation "private": roundup True by unfold_locales rule
     1.9  lemmas true_copy = private.true
    1.10  end
    1.11  
     2.1 --- a/src/HOL/Algebra/Ring.thy	Mon Nov 09 13:49:56 2015 +0100
     2.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Nov 09 15:48:17 2015 +0100
     2.3 @@ -94,7 +94,7 @@
     2.4  text \<open>Transfer facts from multiplicative structures via interpretation.\<close>
     2.5  
     2.6  sublocale abelian_monoid <
     2.7 -  add!: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     2.8 +  add: monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     2.9    rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    2.10      and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    2.11      and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    2.12 @@ -112,7 +112,7 @@
    2.13  end
    2.14  
    2.15  sublocale abelian_monoid <
    2.16 -  add!: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.17 +  add: comm_monoid "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.18    rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    2.19      and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    2.20      and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    2.21 @@ -168,7 +168,7 @@
    2.22  end
    2.23  
    2.24  sublocale abelian_group <
    2.25 -  add!: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.26 +  add: group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.27    rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    2.28      and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    2.29      and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
    2.30 @@ -196,7 +196,7 @@
    2.31  end
    2.32  
    2.33  sublocale abelian_group <
    2.34 -  add!: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.35 +  add: comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    2.36    rewrites "carrier \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = carrier G"
    2.37      and "mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = add G"
    2.38      and "one \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> = zero G"
     3.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Nov 09 13:49:56 2015 +0100
     3.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Mon Nov 09 15:48:17 2015 +0100
     3.3 @@ -498,8 +498,8 @@
     3.4    and     sWELL: "Well_order s"
     3.5  begin
     3.6  
     3.7 -interpretation r!: wo_rel r by unfold_locales (rule rWELL)
     3.8 -interpretation s!: wo_rel s by unfold_locales (rule sWELL)
     3.9 +interpretation r: wo_rel r by unfold_locales (rule rWELL)
    3.10 +interpretation s: wo_rel s by unfold_locales (rule sWELL)
    3.11  
    3.12  abbreviation "SUPP \<equiv> support r.zero (Field s)"
    3.13  abbreviation "FINFUNC \<equiv> FinFunc r s"
    3.14 @@ -1134,8 +1134,8 @@
    3.15    moreover
    3.16    from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce
    3.17    moreover
    3.18 -  interpret t!: wo_rel t by unfold_locales (rule t)
    3.19 -  interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
    3.20 +  interpret t: wo_rel t by unfold_locales (rule t)
    3.21 +  interpret rt: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
    3.22    from *(3) have "ofilter ?R (?f ` Field ?L)"
    3.23      unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
    3.24      by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
    3.25 @@ -1200,8 +1200,8 @@
    3.26    from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
    3.27      by auto (metis well_order_on_domain t, metis well_order_on_domain s)
    3.28    moreover
    3.29 -  interpret t!: wo_rel t by unfold_locales (rule t)
    3.30 -  interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
    3.31 +  interpret t: wo_rel t by unfold_locales (rule t)
    3.32 +  interpret rt: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
    3.33    from *(3) have "ofilter ?R (?f ` Field ?L)"
    3.34      unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
    3.35      by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
    3.36 @@ -1277,12 +1277,12 @@
    3.37    assumes "oone <o r" "s <o t"
    3.38    shows   "r ^o s <o r ^o t" (is "?L <o ?R")
    3.39  proof -
    3.40 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
    3.41 -  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
    3.42 -  interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
    3.43 -  interpret r!: wo_rel r by unfold_locales (rule r)
    3.44 -  interpret s!: wo_rel s by unfold_locales (rule s)
    3.45 -  interpret t!: wo_rel t by unfold_locales (rule t)
    3.46 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
    3.47 +  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
    3.48 +  interpret rexpt: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
    3.49 +  interpret r: wo_rel r by unfold_locales (rule r)
    3.50 +  interpret s: wo_rel s by unfold_locales (rule s)
    3.51 +  interpret t: wo_rel t by unfold_locales (rule t)
    3.52    have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
    3.53    moreover
    3.54    { assume "Field r = {r.zero}"
    3.55 @@ -1388,11 +1388,11 @@
    3.56    assumes "r \<le>o s"
    3.57    shows   "r ^o t \<le>o s ^o t"
    3.58  proof -
    3.59 -  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
    3.60 -  interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t)
    3.61 -  interpret r!: wo_rel r by unfold_locales (rule r)
    3.62 -  interpret s!: wo_rel s by unfold_locales (rule s)
    3.63 -  interpret t!: wo_rel t by unfold_locales (rule t)
    3.64 +  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
    3.65 +  interpret st: wo_rel2 s t by unfold_locales (rule s, rule t)
    3.66 +  interpret r: wo_rel r by unfold_locales (rule r)
    3.67 +  interpret s: wo_rel s by unfold_locales (rule s)
    3.68 +  interpret t: wo_rel t by unfold_locales (rule t)
    3.69    show ?thesis
    3.70    proof (cases "t = {}")
    3.71      case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
    3.72 @@ -1453,9 +1453,9 @@
    3.73    assumes "oone <o r"
    3.74    shows   "s \<le>o r ^o s"
    3.75  proof -
    3.76 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
    3.77 -  interpret r!: wo_rel r by unfold_locales (rule r)
    3.78 -  interpret s!: wo_rel s by unfold_locales (rule s)
    3.79 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
    3.80 +  interpret r: wo_rel r by unfold_locales (rule r)
    3.81 +  interpret s: wo_rel s by unfold_locales (rule s)
    3.82    from assms well_order_on_domain[OF r] obtain x where
    3.83      x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
    3.84      unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
    3.85 @@ -1511,9 +1511,9 @@
    3.86      "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
    3.87    shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
    3.88  proof -
    3.89 -  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
    3.90 -  interpret s!: wo_rel s by unfold_locales (rule s)
    3.91 -  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
    3.92 +  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
    3.93 +  interpret s: wo_rel s by unfold_locales (rule s)
    3.94 +  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
    3.95    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)"
    3.96      using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
    3.97    hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
    3.98 @@ -1535,9 +1535,9 @@
    3.99      "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
   3.100    shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
   3.101  proof -
   3.102 -  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
   3.103 -  interpret t!: wo_rel t by unfold_locales (rule t)
   3.104 -  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   3.105 +  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
   3.106 +  interpret t: wo_rel t by unfold_locales (rule t)
   3.107 +  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   3.108    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)"
   3.109      using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
   3.110    hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
   3.111 @@ -1548,9 +1548,9 @@
   3.112  
   3.113  lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
   3.114  proof (rule ordIso_symmetric)
   3.115 -  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   3.116 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.117 -  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
   3.118 +  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   3.119 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.120 +  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
   3.121    let ?f = "\<lambda>(f, g). case_sum f g"
   3.122    have "bij_betw ?f (Field ?L) (Field ?R)"
   3.123    unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
   3.124 @@ -1581,8 +1581,8 @@
   3.125    assumes Field: "Field r \<noteq> {}"
   3.126    shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
   3.127  proof safe
   3.128 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.129 -  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.130 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.131 +  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.132    fix g assume g: "g \<in> FinFunc r (s *o t)"
   3.133    hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))"
   3.134      unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
   3.135 @@ -1591,8 +1591,8 @@
   3.136      unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
   3.137      by (auto simp: rev_curr_def fin_support_def)
   3.138  next
   3.139 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.140 -  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.141 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.142 +  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.143    fix fg assume *: "fg \<in> FinFunc (r ^o s) t"
   3.144    let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined"
   3.145    show "fg \<in> rev_curr ` FinFunc r (s *o t)"
   3.146 @@ -1631,12 +1631,12 @@
   3.147    shows "wo_rel.max_fun_diff (s *o t) f g =
   3.148      (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
   3.149  proof -
   3.150 -  interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
   3.151 -  interpret s!: wo_rel s by unfold_locales (rule s)
   3.152 -  interpret t!: wo_rel t by unfold_locales (rule t)
   3.153 -  interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
   3.154 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.155 -  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.156 +  interpret st: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
   3.157 +  interpret s: wo_rel s by unfold_locales (rule s)
   3.158 +  interpret t: wo_rel t by unfold_locales (rule t)
   3.159 +  interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
   3.160 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.161 +  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.162    from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
   3.163      have diff1: "rev_curr f \<noteq> rev_curr g"
   3.164        "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
   3.165 @@ -1668,8 +1668,8 @@
   3.166  lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
   3.167  proof (cases "r = {}")
   3.168    case True
   3.169 -  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.170 -  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.171 +  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.172 +  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.173    show ?thesis
   3.174    proof (cases "s = {} \<or> t = {}")
   3.175      case True with `r = {}` show ?thesis
   3.176 @@ -1687,9 +1687,9 @@
   3.177    hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty)
   3.178    show ?thesis
   3.179    proof (rule ordIso_symmetric)
   3.180 -    interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
   3.181 -    interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.182 -    interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.183 +    interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
   3.184 +    interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
   3.185 +    interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   3.186      have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
   3.187      unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
   3.188        show "inj_on rev_curr (FinFunc r (s *o t))"
     4.1 --- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Nov 09 13:49:56 2015 +0100
     4.2 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Mon Nov 09 15:48:17 2015 +0100
     4.3 @@ -932,8 +932,8 @@
     4.4  and f: "\<And> a. a \<in> Field r \<Longrightarrow> f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
     4.5  shows "\<exists> g. embed r s g"
     4.6  proof-
     4.7 -  interpret r!: wo_rel r by unfold_locales (rule r)
     4.8 -  interpret s!: wo_rel s by unfold_locales (rule s)
     4.9 +  interpret r: wo_rel r by unfold_locales (rule r)
    4.10 +  interpret s: wo_rel s by unfold_locales (rule s)
    4.11    let ?G = "\<lambda> g a. suc s (g ` underS r a)"
    4.12    def g \<equiv> "worec r ?G"
    4.13    have adm: "adm_wo r ?G" unfolding r.adm_wo_def image_def by auto
     5.1 --- a/src/HOL/Finite_Set.thy	Mon Nov 09 13:49:56 2015 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Mon Nov 09 15:48:17 2015 +0100
     5.3 @@ -1196,12 +1196,12 @@
     5.4  definition card :: "'a set \<Rightarrow> nat" where
     5.5    "card = folding.F (\<lambda>_. Suc) 0"
     5.6  
     5.7 -interpretation card!: folding "\<lambda>_. Suc" 0
     5.8 +interpretation card: folding "\<lambda>_. Suc" 0
     5.9  rewrites
    5.10    "folding.F (\<lambda>_. Suc) 0 = card"
    5.11  proof -
    5.12    show "folding (\<lambda>_. Suc)" by standard rule
    5.13 -  then interpret card!: folding "\<lambda>_. Suc" 0 .
    5.14 +  then interpret card: folding "\<lambda>_. Suc" 0 .
    5.15    from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
    5.16  qed
    5.17  
     6.1 --- a/src/HOL/GCD.thy	Mon Nov 09 13:49:56 2015 +0100
     6.2 +++ b/src/HOL/GCD.thy	Mon Nov 09 15:48:17 2015 +0100
     6.3 @@ -104,7 +104,7 @@
     6.4    "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
     6.5    by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
     6.6  
     6.7 -sublocale gcd!: abel_semigroup gcd
     6.8 +sublocale gcd: abel_semigroup gcd
     6.9  proof
    6.10    fix a b c
    6.11    show "gcd a b = gcd b a"
    6.12 @@ -256,7 +256,7 @@
    6.13    "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
    6.14    by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
    6.15  
    6.16 -sublocale lcm!: abel_semigroup lcm
    6.17 +sublocale lcm: abel_semigroup lcm
    6.18  proof
    6.19    fix a b c
    6.20    show "lcm a b = lcm b a"
     7.1 --- a/src/HOL/Groups.thy	Mon Nov 09 13:49:56 2015 +0100
     7.2 +++ b/src/HOL/Groups.thy	Mon Nov 09 15:48:17 2015 +0100
     7.3 @@ -131,7 +131,7 @@
     7.4    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
     7.5  begin
     7.6  
     7.7 -sublocale add!: semigroup plus
     7.8 +sublocale add: semigroup plus
     7.9    by standard (fact add_assoc)
    7.10  
    7.11  end
    7.12 @@ -142,7 +142,7 @@
    7.13    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    7.14  begin
    7.15  
    7.16 -sublocale add!: abel_semigroup plus
    7.17 +sublocale add: abel_semigroup plus
    7.18    by standard (fact add_commute)
    7.19  
    7.20  declare add.left_commute [algebra_simps, field_simps]
    7.21 @@ -159,7 +159,7 @@
    7.22    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    7.23  begin
    7.24  
    7.25 -sublocale mult!: semigroup times
    7.26 +sublocale mult: semigroup times
    7.27    by standard (fact mult_assoc)
    7.28  
    7.29  end
    7.30 @@ -170,7 +170,7 @@
    7.31    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    7.32  begin
    7.33  
    7.34 -sublocale mult!: abel_semigroup times
    7.35 +sublocale mult: abel_semigroup times
    7.36    by standard (fact mult_commute)
    7.37  
    7.38  declare mult.left_commute [algebra_simps, field_simps]
    7.39 @@ -188,7 +188,7 @@
    7.40      and add_0_right: "a + 0 = a"
    7.41  begin
    7.42  
    7.43 -sublocale add!: monoid plus 0
    7.44 +sublocale add: monoid plus 0
    7.45    by standard (fact add_0_left add_0_right)+
    7.46  
    7.47  end
    7.48 @@ -203,7 +203,7 @@
    7.49  subclass monoid_add
    7.50    by standard (simp_all add: add_0 add.commute [of _ 0])
    7.51  
    7.52 -sublocale add!: comm_monoid plus 0
    7.53 +sublocale add: comm_monoid plus 0
    7.54    by standard (simp add: ac_simps)
    7.55  
    7.56  end
    7.57 @@ -213,7 +213,7 @@
    7.58      and mult_1_right: "a * 1 = a"
    7.59  begin
    7.60  
    7.61 -sublocale mult!: monoid times 1
    7.62 +sublocale mult: monoid times 1
    7.63    by standard (fact mult_1_left mult_1_right)+
    7.64  
    7.65  end
    7.66 @@ -228,7 +228,7 @@
    7.67  subclass monoid_mult
    7.68    by standard (simp_all add: mult_1 mult.commute [of _ 1])
    7.69  
    7.70 -sublocale mult!: comm_monoid times 1
    7.71 +sublocale mult: comm_monoid times 1
    7.72    by standard (simp add: ac_simps)
    7.73  
    7.74  end
     8.1 --- a/src/HOL/Groups_Big.thy	Mon Nov 09 13:49:56 2015 +0100
     8.2 +++ b/src/HOL/Groups_Big.thy	Mon Nov 09 15:48:17 2015 +0100
     8.3 @@ -471,12 +471,12 @@
     8.4  where
     8.5    "setsum = comm_monoid_set.F plus 0"
     8.6  
     8.7 -sublocale setsum!: comm_monoid_set plus 0
     8.8 +sublocale setsum: comm_monoid_set plus 0
     8.9  rewrites
    8.10    "comm_monoid_set.F plus 0 = setsum"
    8.11  proof -
    8.12    show "comm_monoid_set plus 0" ..
    8.13 -  then interpret setsum!: comm_monoid_set plus 0 .
    8.14 +  then interpret setsum: comm_monoid_set plus 0 .
    8.15    from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    8.16  qed
    8.17  
    8.18 @@ -1062,12 +1062,12 @@
    8.19  where
    8.20    "setprod = comm_monoid_set.F times 1"
    8.21  
    8.22 -sublocale setprod!: comm_monoid_set times 1
    8.23 +sublocale setprod: comm_monoid_set times 1
    8.24  rewrites
    8.25    "comm_monoid_set.F times 1 = setprod"
    8.26  proof -
    8.27    show "comm_monoid_set times 1" ..
    8.28 -  then interpret setprod!: comm_monoid_set times 1 .
    8.29 +  then interpret setprod: comm_monoid_set times 1 .
    8.30    from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    8.31  qed
    8.32  
     9.1 --- a/src/HOL/Groups_List.thy	Mon Nov 09 13:49:56 2015 +0100
     9.2 +++ b/src/HOL/Groups_List.thy	Mon Nov 09 15:48:17 2015 +0100
     9.3 @@ -65,12 +65,12 @@
     9.4  where
     9.5    "listsum  = monoid_list.F plus 0"
     9.6  
     9.7 -sublocale listsum!: monoid_list plus 0
     9.8 +sublocale listsum: monoid_list plus 0
     9.9  rewrites
    9.10   "monoid_list.F plus 0 = listsum"
    9.11  proof -
    9.12    show "monoid_list plus 0" ..
    9.13 -  then interpret listsum!: monoid_list plus 0 .
    9.14 +  then interpret listsum: monoid_list plus 0 .
    9.15    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    9.16  qed
    9.17   
    9.18 @@ -79,22 +79,22 @@
    9.19  context comm_monoid_add
    9.20  begin
    9.21  
    9.22 -sublocale listsum!: comm_monoid_list plus 0
    9.23 +sublocale listsum: comm_monoid_list plus 0
    9.24  rewrites
    9.25    "monoid_list.F plus 0 = listsum"
    9.26  proof -
    9.27    show "comm_monoid_list plus 0" ..
    9.28 -  then interpret listsum!: comm_monoid_list plus 0 .
    9.29 +  then interpret listsum: comm_monoid_list plus 0 .
    9.30    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    9.31  qed
    9.32  
    9.33 -sublocale setsum!: comm_monoid_list_set plus 0
    9.34 +sublocale setsum: comm_monoid_list_set plus 0
    9.35  rewrites
    9.36    "monoid_list.F plus 0 = listsum"
    9.37    and "comm_monoid_set.F plus 0 = setsum"
    9.38  proof -
    9.39    show "comm_monoid_list_set plus 0" ..
    9.40 -  then interpret setsum!: comm_monoid_list_set plus 0 .
    9.41 +  then interpret setsum: comm_monoid_list_set plus 0 .
    9.42    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    9.43    from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    9.44  qed
    9.45 @@ -332,12 +332,12 @@
    9.46  where
    9.47    "listprod  = monoid_list.F times 1"
    9.48  
    9.49 -sublocale listprod!: monoid_list times 1
    9.50 +sublocale listprod: monoid_list times 1
    9.51  rewrites
    9.52    "monoid_list.F times 1 = listprod"
    9.53  proof -
    9.54    show "monoid_list times 1" ..
    9.55 -  then interpret listprod!: monoid_list times 1 .
    9.56 +  then interpret listprod: monoid_list times 1 .
    9.57    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    9.58  qed
    9.59  
    9.60 @@ -346,22 +346,22 @@
    9.61  context comm_monoid_mult
    9.62  begin
    9.63  
    9.64 -sublocale listprod!: comm_monoid_list times 1
    9.65 +sublocale listprod: comm_monoid_list times 1
    9.66  rewrites
    9.67    "monoid_list.F times 1 = listprod"
    9.68  proof -
    9.69    show "comm_monoid_list times 1" ..
    9.70 -  then interpret listprod!: comm_monoid_list times 1 .
    9.71 +  then interpret listprod: comm_monoid_list times 1 .
    9.72    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    9.73  qed
    9.74  
    9.75 -sublocale setprod!: comm_monoid_list_set times 1
    9.76 +sublocale setprod: comm_monoid_list_set times 1
    9.77  rewrites
    9.78    "monoid_list.F times 1 = listprod"
    9.79    and "comm_monoid_set.F times 1 = setprod"
    9.80  proof -
    9.81    show "comm_monoid_list_set times 1" ..
    9.82 -  then interpret setprod!: comm_monoid_list_set times 1 .
    9.83 +  then interpret setprod: comm_monoid_list_set times 1 .
    9.84    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    9.85    from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    9.86  qed
    10.1 --- a/src/HOL/HOLCF/Universal.thy	Mon Nov 09 13:49:56 2015 +0100
    10.2 +++ b/src/HOL/HOLCF/Universal.thy	Mon Nov 09 15:48:17 2015 +0100
    10.3 @@ -836,7 +836,7 @@
    10.4  
    10.5  end
    10.6  
    10.7 -interpretation compact_basis!:
    10.8 +interpretation compact_basis:
    10.9    ideal_completion below Rep_compact_basis
   10.10      "approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set"
   10.11  proof -
    11.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 09 13:49:56 2015 +0100
    11.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 09 15:48:17 2015 +0100
    11.3 @@ -404,7 +404,7 @@
    11.4      by (simp only: Heap_ord_def Heap_lub_def)
    11.5  qed
    11.6  
    11.7 -interpretation heap!: partial_function_definitions Heap_ord Heap_lub
    11.8 +interpretation heap: partial_function_definitions Heap_ord Heap_lub
    11.9    rewrites "Heap_lub {} \<equiv> Heap Map.empty"
   11.10  by (fact heap_interpretation)(simp add: Heap_lub_empty)
   11.11  
    12.1 --- a/src/HOL/Lattices.thy	Mon Nov 09 13:49:56 2015 +0100
    12.2 +++ b/src/HOL/Lattices.thy	Mon Nov 09 15:48:17 2015 +0100
    12.3 @@ -271,7 +271,7 @@
    12.4  context semilattice_inf
    12.5  begin
    12.6  
    12.7 -sublocale inf!: semilattice inf
    12.8 +sublocale inf: semilattice inf
    12.9  proof
   12.10    fix a b c
   12.11    show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
   12.12 @@ -282,7 +282,7 @@
   12.13      by (rule antisym) (auto simp add: le_inf_iff)
   12.14  qed
   12.15  
   12.16 -sublocale inf!: semilattice_order inf less_eq less
   12.17 +sublocale inf: semilattice_order inf less_eq less
   12.18    by standard (auto simp add: le_iff_inf less_le)
   12.19  
   12.20  lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   12.21 @@ -316,7 +316,7 @@
   12.22  context semilattice_sup
   12.23  begin
   12.24  
   12.25 -sublocale sup!: semilattice sup
   12.26 +sublocale sup: semilattice sup
   12.27  proof
   12.28    fix a b c
   12.29    show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   12.30 @@ -327,7 +327,7 @@
   12.31      by (rule antisym) (auto simp add: le_sup_iff)
   12.32  qed
   12.33  
   12.34 -sublocale sup!: semilattice_order sup greater_eq greater
   12.35 +sublocale sup: semilattice_order sup greater_eq greater
   12.36    by standard (auto simp add: le_iff_sup sup.commute less_le)
   12.37  
   12.38  lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   12.39 @@ -484,8 +484,8 @@
   12.40  class bounded_semilattice_inf_top = semilattice_inf + order_top
   12.41  begin
   12.42  
   12.43 -sublocale inf_top!: semilattice_neutr inf top
   12.44 -  + inf_top!: semilattice_neutr_order inf top less_eq less
   12.45 +sublocale inf_top: semilattice_neutr inf top
   12.46 +  + inf_top: semilattice_neutr_order inf top less_eq less
   12.47  proof
   12.48    fix x
   12.49    show "x \<sqinter> \<top> = x"
   12.50 @@ -497,8 +497,8 @@
   12.51  class bounded_semilattice_sup_bot = semilattice_sup + order_bot
   12.52  begin
   12.53  
   12.54 -sublocale sup_bot!: semilattice_neutr sup bot
   12.55 -  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
   12.56 +sublocale sup_bot: semilattice_neutr sup bot
   12.57 +  + sup_bot: semilattice_neutr_order sup bot greater_eq greater
   12.58  proof
   12.59    fix x
   12.60    show "x \<squnion> \<bottom> = x"
   12.61 @@ -715,8 +715,8 @@
   12.62  context linorder
   12.63  begin
   12.64  
   12.65 -sublocale min!: semilattice_order min less_eq less
   12.66 -  + max!: semilattice_order max greater_eq greater
   12.67 +sublocale min: semilattice_order min less_eq less
   12.68 +  + max: semilattice_order max greater_eq greater
   12.69    by standard (auto simp add: min_def max_def)
   12.70  
   12.71  lemma min_le_iff_disj:
    13.1 --- a/src/HOL/Lattices_Big.thy	Mon Nov 09 13:49:56 2015 +0100
    13.2 +++ b/src/HOL/Lattices_Big.thy	Mon Nov 09 15:48:17 2015 +0100
    13.3 @@ -318,12 +318,12 @@
    13.4  where
    13.5    "Inf_fin = semilattice_set.F inf"
    13.6  
    13.7 -sublocale Inf_fin!: semilattice_order_set inf less_eq less
    13.8 +sublocale Inf_fin: semilattice_order_set inf less_eq less
    13.9  rewrites
   13.10    "semilattice_set.F inf = Inf_fin"
   13.11  proof -
   13.12    show "semilattice_order_set inf less_eq less" ..
   13.13 -  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   13.14 +  then interpret Inf_fin: semilattice_order_set inf less_eq less .
   13.15    from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   13.16  qed
   13.17  
   13.18 @@ -336,12 +336,12 @@
   13.19  where
   13.20    "Sup_fin = semilattice_set.F sup"
   13.21  
   13.22 -sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
   13.23 +sublocale Sup_fin: semilattice_order_set sup greater_eq greater
   13.24  rewrites
   13.25    "semilattice_set.F sup = Sup_fin"
   13.26  proof -
   13.27    show "semilattice_order_set sup greater_eq greater" ..
   13.28 -  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   13.29 +  then interpret Sup_fin: semilattice_order_set sup greater_eq greater .
   13.30    from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   13.31  qed
   13.32  
   13.33 @@ -490,16 +490,16 @@
   13.34  where
   13.35    "Max = semilattice_set.F max"
   13.36  
   13.37 -sublocale Min!: semilattice_order_set min less_eq less
   13.38 -  + Max!: semilattice_order_set max greater_eq greater
   13.39 +sublocale Min: semilattice_order_set min less_eq less
   13.40 +  + Max: semilattice_order_set max greater_eq greater
   13.41  rewrites
   13.42    "semilattice_set.F min = Min"
   13.43    and "semilattice_set.F max = Max"
   13.44  proof -
   13.45    show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
   13.46 -  then interpret Min!: semilattice_order_set min less_eq less .
   13.47 +  then interpret Min: semilattice_order_set min less_eq less .
   13.48    show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
   13.49 -  then interpret Max!: semilattice_order_set max greater_eq greater .
   13.50 +  then interpret Max: semilattice_order_set max greater_eq greater .
   13.51    from Min_def show "semilattice_set.F min = Min" by rule
   13.52    from Max_def show "semilattice_set.F max = Max" by rule
   13.53  qed
   13.54 @@ -530,14 +530,14 @@
   13.55  lemma dual_Min:
   13.56    "linorder.Min greater_eq = Max"
   13.57  proof -
   13.58 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   13.59 +  interpret dual: linorder greater_eq greater by (fact dual_linorder)
   13.60    show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   13.61  qed
   13.62  
   13.63  lemma dual_Max:
   13.64    "linorder.Max greater_eq = Min"
   13.65  proof -
   13.66 -  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   13.67 +  interpret dual: linorder greater_eq greater by (fact dual_linorder)
   13.68    show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   13.69  qed
   13.70  
    14.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 09 13:49:56 2015 +0100
    14.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 09 15:48:17 2015 +0100
    14.3 @@ -26,10 +26,10 @@
    14.4    assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
    14.5  begin
    14.6  
    14.7 -sublocale conj!: abel_semigroup conj
    14.8 +sublocale conj: abel_semigroup conj
    14.9    by standard (fact conj_assoc conj_commute)+
   14.10  
   14.11 -sublocale disj!: abel_semigroup disj
   14.12 +sublocale disj: abel_semigroup disj
   14.13    by standard (fact disj_assoc disj_commute)+
   14.14  
   14.15  lemmas conj_left_commute = conj.left_commute
   14.16 @@ -190,7 +190,7 @@
   14.17    assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
   14.18  begin
   14.19  
   14.20 -sublocale xor!: abel_semigroup xor
   14.21 +sublocale xor: abel_semigroup xor
   14.22  proof
   14.23    fix x y z :: 'a
   14.24    let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
    15.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Nov 09 13:49:56 2015 +0100
    15.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Nov 09 15:48:17 2015 +0100
    15.3 @@ -20,7 +20,7 @@
    15.4  where
    15.5    expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
    15.6  
    15.7 -interpretation F!: comm_monoid_set f 1
    15.8 +interpretation F: comm_monoid_set f 1
    15.9    ..
   15.10  
   15.11  lemma expand_superset:
   15.12 @@ -225,13 +225,13 @@
   15.13  where
   15.14    "Sum_any = comm_monoid_fun.G plus 0"
   15.15  
   15.16 -permanent_interpretation Sum_any!: comm_monoid_fun plus 0
   15.17 +permanent_interpretation Sum_any: comm_monoid_fun plus 0
   15.18  where
   15.19    "comm_monoid_fun.G plus 0 = Sum_any" and
   15.20    "comm_monoid_set.F plus 0 = setsum"
   15.21  proof -
   15.22    show "comm_monoid_fun plus 0" ..
   15.23 -  then interpret Sum_any!: comm_monoid_fun plus 0 .
   15.24 +  then interpret Sum_any: comm_monoid_fun plus 0 .
   15.25    from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
   15.26    from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   15.27  qed
   15.28 @@ -298,13 +298,13 @@
   15.29  where
   15.30    "Prod_any = comm_monoid_fun.G times 1"
   15.31  
   15.32 -permanent_interpretation Prod_any!: comm_monoid_fun times 1
   15.33 +permanent_interpretation Prod_any: comm_monoid_fun times 1
   15.34  where
   15.35    "comm_monoid_fun.G times 1 = Prod_any" and
   15.36    "comm_monoid_set.F times 1 = setprod"
   15.37  proof -
   15.38    show "comm_monoid_fun times 1" ..
   15.39 -  then interpret Prod_any!: comm_monoid_fun times 1 .
   15.40 +  then interpret Prod_any: comm_monoid_fun times 1 .
   15.41    from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
   15.42    from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
   15.43  qed
    16.1 --- a/src/HOL/Library/Multiset.thy	Mon Nov 09 13:49:56 2015 +0100
    16.2 +++ b/src/HOL/Library/Multiset.thy	Mon Nov 09 15:48:17 2015 +0100
    16.3 @@ -1058,7 +1058,7 @@
    16.4  where
    16.5    "mset_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
    16.6  
    16.7 -interpretation mset_set!: folding "\<lambda>x M. {#x#} + M" "{#}"
    16.8 +interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
    16.9  rewrites
   16.10    "folding.F (\<lambda>x M. {#x#} + M) {#} = mset_set"
   16.11  proof -
   16.12 @@ -1221,7 +1221,7 @@
   16.13  definition msetsum :: "'a multiset \<Rightarrow> 'a"
   16.14    where "msetsum = comm_monoid_mset.F plus 0"
   16.15  
   16.16 -sublocale msetsum!: comm_monoid_mset plus 0
   16.17 +sublocale msetsum: comm_monoid_mset plus 0
   16.18    rewrites "comm_monoid_mset.F plus 0 = msetsum"
   16.19  proof -
   16.20    show "comm_monoid_mset plus 0" ..
   16.21 @@ -1279,7 +1279,7 @@
   16.22  definition msetprod :: "'a multiset \<Rightarrow> 'a"
   16.23    where "msetprod = comm_monoid_mset.F times 1"
   16.24  
   16.25 -sublocale msetprod!: comm_monoid_mset times 1
   16.26 +sublocale msetprod: comm_monoid_mset times 1
   16.27    rewrites "comm_monoid_mset.F times 1 = msetprod"
   16.28  proof -
   16.29    show "comm_monoid_mset times 1" ..
    17.1 --- a/src/HOL/Library/Polynomial.thy	Mon Nov 09 13:49:56 2015 +0100
    17.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Nov 09 15:48:17 2015 +0100
    17.3 @@ -1887,7 +1887,7 @@
    17.4      by (rule poly_dvd_antisym)
    17.5  qed
    17.6  
    17.7 -interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
    17.8 +interpretation gcd_poly: abel_semigroup "gcd :: _ poly \<Rightarrow> _"
    17.9  proof
   17.10    fix x y z :: "'a poly"
   17.11    show "gcd (gcd x y) z = gcd x (gcd y z)"
    18.1 --- a/src/HOL/Library/Saturated.thy	Mon Nov 09 13:49:56 2015 +0100
    18.2 +++ b/src/HOL/Library/Saturated.thy	Mon Nov 09 15:48:17 2015 +0100
    18.3 @@ -214,7 +214,7 @@
    18.4  
    18.5  end
    18.6  
    18.7 -interpretation Inf_sat!: semilattice_neutr_set min "top :: 'a::len sat"
    18.8 +interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
    18.9  rewrites
   18.10    "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
   18.11  proof -
   18.12 @@ -224,7 +224,7 @@
   18.13      by (simp add: Inf_sat_def)
   18.14  qed
   18.15  
   18.16 -interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
   18.17 +interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
   18.18  rewrites
   18.19    "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
   18.20  proof -
    19.1 --- a/src/HOL/List.thy	Mon Nov 09 13:49:56 2015 +0100
    19.2 +++ b/src/HOL/List.thy	Mon Nov 09 15:48:17 2015 +0100
    19.3 @@ -5150,7 +5150,7 @@
    19.4  definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
    19.5    "sorted_list_of_set = folding.F insort []"
    19.6  
    19.7 -sublocale sorted_list_of_set!: folding insort Nil
    19.8 +sublocale sorted_list_of_set: folding insort Nil
    19.9  rewrites
   19.10    "folding.F insort [] = sorted_list_of_set"
   19.11  proof -
    20.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 09 13:49:56 2015 +0100
    20.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 09 15:48:17 2015 +0100
    20.3 @@ -238,7 +238,7 @@
    20.4    shows "c = gcd a b"
    20.5    by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
    20.6  
    20.7 -sublocale gcd!: abel_semigroup gcd
    20.8 +sublocale gcd: abel_semigroup gcd
    20.9  proof
   20.10    fix a b c 
   20.11    show "gcd (gcd a b) c = gcd a (gcd b c)"
   20.12 @@ -790,7 +790,7 @@
   20.13    shows "c = lcm a b"
   20.14    by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   20.15  
   20.16 -sublocale lcm!: abel_semigroup lcm ..
   20.17 +sublocale lcm: abel_semigroup lcm ..
   20.18  
   20.19  lemma dvd_lcm_D1:
   20.20    "lcm m n dvd k \<Longrightarrow> m dvd k"
    21.1 --- a/src/HOL/Orderings.thy	Mon Nov 09 13:49:56 2015 +0100
    21.2 +++ b/src/HOL/Orderings.thy	Mon Nov 09 15:48:17 2015 +0100
    21.3 @@ -191,7 +191,7 @@
    21.4  lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    21.5    by (auto simp add: less_le_not_le intro: antisym)
    21.6  
    21.7 -sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    21.8 +sublocale order: ordering less_eq less +  dual_order: ordering greater_eq greater
    21.9    by standard (auto intro: antisym order_trans simp add: less_le)
   21.10  
   21.11  
   21.12 @@ -1181,7 +1181,7 @@
   21.13    assumes bot_least: "\<bottom> \<le> a"
   21.14  begin
   21.15  
   21.16 -sublocale bot!: ordering_top greater_eq greater bot
   21.17 +sublocale bot: ordering_top greater_eq greater bot
   21.18    by standard (fact bot_least)
   21.19  
   21.20  lemma le_bot:
   21.21 @@ -1209,7 +1209,7 @@
   21.22    assumes top_greatest: "a \<le> \<top>"
   21.23  begin
   21.24  
   21.25 -sublocale top!: ordering_top less_eq less top
   21.26 +sublocale top: ordering_top less_eq less top
   21.27    by standard (fact top_greatest)
   21.28  
   21.29  lemma top_le:
    22.1 --- a/src/HOL/Partial_Function.thy	Mon Nov 09 13:49:56 2015 +0100
    22.2 +++ b/src/HOL/Partial_Function.thy	Mon Nov 09 15:48:17 2015 +0100
    22.3 @@ -281,12 +281,12 @@
    22.4  lemma antisymP_flat_ord: "antisymP (flat_ord a)"
    22.5  by(rule antisymI)(auto dest: flat_ord_antisym)
    22.6  
    22.7 -interpretation tailrec!:
    22.8 +interpretation tailrec:
    22.9    partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   22.10    rewrites "flat_lub undefined {} \<equiv> undefined"
   22.11  by (rule flat_interpretation)(simp add: flat_lub_def)
   22.12  
   22.13 -interpretation option!:
   22.14 +interpretation option:
   22.15    partial_function_definitions "flat_ord None" "flat_lub None"
   22.16    rewrites "flat_lub None {} \<equiv> None"
   22.17  by (rule flat_interpretation)(simp add: flat_lub_def)
    23.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 09 13:49:56 2015 +0100
    23.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 09 15:48:17 2015 +0100
    23.3 @@ -709,7 +709,7 @@
    23.4  lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
    23.5    by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ereal_def[symmetric])
    23.6  
    23.7 -interpretation lborel!: sigma_finite_measure lborel
    23.8 +interpretation lborel: sigma_finite_measure lborel
    23.9    by (rule sigma_finite_lborel)
   23.10  
   23.11  interpretation lborel_pair: pair_sigma_finite lborel lborel ..
    24.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 13:49:56 2015 +0100
    24.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 09 15:48:17 2015 +0100
    24.3 @@ -113,10 +113,10 @@
    24.4  lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
    24.5    using pmf.measure_pmf[of p] by auto
    24.6  
    24.7 -interpretation measure_pmf!: prob_space "measure_pmf M" for M
    24.8 +interpretation measure_pmf: prob_space "measure_pmf M" for M
    24.9    by (rule prob_space_measure_pmf)
   24.10  
   24.11 -interpretation measure_pmf!: subprob_space "measure_pmf M" for M
   24.12 +interpretation measure_pmf: subprob_space "measure_pmf M" for M
   24.13    by (rule prob_space_imp_subprob_space) unfold_locales
   24.14  
   24.15  lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
    25.1 --- a/src/HOL/Probability/Probability_Measure.thy	Mon Nov 09 13:49:56 2015 +0100
    25.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Mon Nov 09 15:48:17 2015 +0100
    25.3 @@ -46,7 +46,7 @@
    25.4  lemma prob_space_distrD:
    25.5    assumes f: "f \<in> measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
    25.6  proof
    25.7 -  interpret M!: prob_space "distr M N f" by fact
    25.8 +  interpret M: prob_space "distr M N f" by fact
    25.9    have "f -` space N \<inter> space M = space M"
   25.10      using f[THEN measurable_space] by auto
   25.11    then show "emeasure M (space M) = 1"
    26.1 --- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 13:49:56 2015 +0100
    26.2 +++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 15:48:17 2015 +0100
    26.3 @@ -97,7 +97,7 @@
    26.4      by simp
    26.5  qed (force simp: generator.simps prod_emb_empty[symmetric])
    26.6  
    26.7 -interpretation generator!: algebra "space (PiM I M)" generator
    26.8 +interpretation generator: algebra "space (PiM I M)" generator
    26.9    by (rule algebra_generator)
   26.10  
   26.11  lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
   26.12 @@ -407,7 +407,7 @@
   26.13  definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   26.14    "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
   26.15  
   26.16 -sublocale PF!: projective_family UNIV CI
   26.17 +sublocale PF: projective_family UNIV CI
   26.18    unfolding projective_family_def
   26.19  proof safe
   26.20    show "finite J \<Longrightarrow> prob_space (CI J)" for J
   26.21 @@ -460,7 +460,7 @@
   26.22    also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
   26.23    proof (intro INF_greatest)
   26.24      fix n
   26.25 -    interpret C!: prob_space "C 0 n (\<lambda>x. undefined)"
   26.26 +    interpret C: prob_space "C 0 n (\<lambda>x. undefined)"
   26.27        by (rule prob_space_C) simp
   26.28      show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
   26.29      proof cases
   26.30 @@ -606,9 +606,9 @@
   26.31        using count by (auto simp: t_def)
   26.32      then have inj_t_J: "inj_on t (J i)" for i
   26.33        by (rule subset_inj_on) auto
   26.34 -    interpret IT!: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
   26.35 +    interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
   26.36        by standard auto
   26.37 -    interpret Mf!: product_prob_space "\<lambda>x. M (f x)" UNIV
   26.38 +    interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
   26.39        by standard
   26.40      have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
   26.41      proof (induction n)
    27.1 --- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 09 13:49:56 2015 +0100
    27.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 09 15:48:17 2015 +0100
    27.3 @@ -469,7 +469,7 @@
    27.4  hide_const (open) domain
    27.5  hide_const (open) basis_finmap
    27.6  
    27.7 -sublocale polish_projective \<subseteq> P!: prob_space lim
    27.8 +sublocale polish_projective \<subseteq> P: prob_space lim
    27.9  proof
   27.10    have *: "emb I {} {\<lambda>x. undefined} = space (\<Pi>\<^sub>M i\<in>I. borel)"
   27.11      by (auto simp: prod_emb_def space_PiM)
    28.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Nov 09 13:49:56 2015 +0100
    28.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Nov 09 15:48:17 2015 +0100
    28.3 @@ -935,7 +935,7 @@
    28.4      by (auto intro: density_cong)
    28.5  next
    28.6    assume eq: "density M f = density M g"
    28.7 -  interpret f!: sigma_finite_measure "density M f" by fact
    28.8 +  interpret f: sigma_finite_measure "density M f" by fact
    28.9    from f.sigma_finite_incseq guess A . note cover = this
   28.10  
   28.11    have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
    29.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 13:49:56 2015 +0100
    29.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 15:48:17 2015 +0100
    29.3 @@ -1479,7 +1479,7 @@
    29.4  lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
    29.5    by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
    29.6  
    29.7 -interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
    29.8 +interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
    29.9    using measure_space[of M] by (auto simp: measure_space_def)
   29.10  
   29.11  definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where