--- 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
--- 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"
--- 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))"
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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 -
--- 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)
--- 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:
--- 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
--- 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>
--- 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
--- 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" ..
--- 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)"
--- 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 -
--- 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 -
--- 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"
--- 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:
--- 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)
--- 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 ..
--- 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)"
--- 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"
--- 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)
--- 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)
--- 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"
--- 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