# HG changeset patch
# User haftmann
# Date 1465654962 -7200
# Node ID 9ac558ab0906aca7ff4ec1a8a0b4a494202f396b
# Parent  26134a00d06015c7271d842ac95b8674ca210e7e
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

diff -r 26134a00d060 -r 9ac558ab0906 NEWS
--- a/NEWS	Sat Jun 11 17:40:52 2016 +0200
+++ b/NEWS	Sat Jun 11 16:22:42 2016 +0200
@@ -132,6 +132,14 @@
 
 *** HOL ***
 
+* Abstract locales semigroup, abel_semigroup, semilattice,
+semilattice_neutr, ordering, ordering_top, semilattice_order,
+semilattice_neutr_order, comm_monoid_set, semilattice_set,
+semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set
+monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,
+comm_monoid_fun use boldified syntax uniformly that does not clash
+with corresponding global syntax.  INCOMPATIBILITY.
+
 * Conventional syntax "%(). t" for unit abstractions.  Slight syntactic
 INCOMPATIBILITY.
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -42,17 +42,17 @@
 \<close>
 
 locale semigroup =
-  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
+  assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
 
 locale abel_semigroup = semigroup +
-  assumes commute [ac_simps]: "a * b = b * a"
+  assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
 begin
 
 lemma left_commute [ac_simps]:
-  "b * (a * c) = a * (b * c)"
+  "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
 proof -
-  have "(b * a) * c = (a * b) * c"
+  have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
     by (simp only: commute)
   then show ?thesis
     by (simp only: assoc)
@@ -61,13 +61,13 @@
 end
 
 locale monoid = semigroup +
-  fixes z :: 'a ("1")
-  assumes left_neutral [simp]: "1 * a = a"
-  assumes right_neutral [simp]: "a * 1 = a"
+  fixes z :: 'a ("\<^bold>1")
+  assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
+  assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
 
 locale comm_monoid = abel_semigroup +
-  fixes z :: 'a ("1")
-  assumes comm_neutral: "a * 1 = a"
+  fixes z :: 'a ("\<^bold>1")
+  assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
 begin
 
 sublocale monoid
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -11,9 +11,6 @@
 
 subsection \<open>Generic monoid operation over a set\<close>
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
 locale comm_monoid_set = comm_monoid
 begin
 
@@ -25,24 +22,24 @@
 
 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
 where
-  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
+  eq_fold: "F g A = Finite_Set.fold (f \<circ> g) \<^bold>1 A"
 
 lemma infinite [simp]:
-  "\<not> finite A \<Longrightarrow> F g A = 1"
+  "\<not> finite A \<Longrightarrow> F g A = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma empty [simp]:
-  "F g {} = 1"
+  "F g {} = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma insert [simp]:
   assumes "finite A" and "x \<notin> A"
-  shows "F g (insert x A) = g x * F g A"
+  shows "F g (insert x A) = g x \<^bold>* F g A"
   using assms by (simp add: eq_fold)
 
 lemma remove:
   assumes "finite A" and "x \<in> A"
-  shows "F g A = g x * F g (A - {x})"
+  shows "F g A = g x \<^bold>* F g (A - {x})"
 proof -
   from \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
     by (auto dest: mk_disjoint_insert)
@@ -52,21 +49,21 @@
 
 lemma insert_remove:
   assumes "finite A"
-  shows "F g (insert x A) = g x * F g (A - {x})"
+  shows "F g (insert x A) = g x \<^bold>* F g (A - {x})"
   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
 
 lemma neutral:
-  assumes "\<forall>x\<in>A. g x = 1"
-  shows "F g A = 1"
+  assumes "\<forall>x\<in>A. g x = \<^bold>1"
+  shows "F g A = \<^bold>1"
   using assms by (induct A rule: infinite_finite_induct) simp_all
 
 lemma neutral_const [simp]:
-  "F (\<lambda>_. 1) A = 1"
+  "F (\<lambda>_. \<^bold>1) A = \<^bold>1"
   by (simp add: neutral)
 
 lemma union_inter:
   assumes "finite A" and "finite B"
-  shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
+  shows "F g (A \<union> B) \<^bold>* F g (A \<inter> B) = F g A \<^bold>* F g B"
   \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
 using assms proof (induct A)
   case empty then show ?case by simp
@@ -77,19 +74,19 @@
 
 corollary union_inter_neutral:
   assumes "finite A" and "finite B"
-  and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
-  shows "F g (A \<union> B) = F g A * F g B"
+  and I0: "\<forall>x \<in> A \<inter> B. g x = \<^bold>1"
+  shows "F g (A \<union> B) = F g A \<^bold>* F g B"
   using assms by (simp add: union_inter [symmetric] neutral)
 
 corollary union_disjoint:
   assumes "finite A" and "finite B"
   assumes "A \<inter> B = {}"
-  shows "F g (A \<union> B) = F g A * F g B"
+  shows "F g (A \<union> B) = F g A \<^bold>* F g B"
   using assms by (simp add: union_inter_neutral)
 
 lemma union_diff2:
   assumes "finite A" and "finite B"
-  shows "F g (A \<union> B) = F g (A - B) * F g (B - A) * F g (A \<inter> B)"
+  shows "F g (A \<union> B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \<inter> B)"
 proof -
   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
     by auto
@@ -98,12 +95,12 @@
 
 lemma subset_diff:
   assumes "B \<subseteq> A" and "finite A"
-  shows "F g A = F g (A - B) * F g B"
+  shows "F g A = F g (A - B) \<^bold>* F g B"
 proof -
   from assms have "finite (A - B)" by auto
   moreover from assms have "finite B" by (rule finite_subset)
   moreover from assms have "(A - B) \<inter> B = {}" by auto
-  ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
+  ultimately have "F g (A - B \<union> B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint)
   moreover from assms have "A \<union> B = A" by auto
   ultimately show ?thesis by simp
 qed
@@ -114,10 +111,10 @@
   using assms by (induct A) (simp_all add: insert_Diff_if)
 
 lemma not_neutral_contains_not_neutral:
-  assumes "F g A \<noteq> z"
-  obtains a where "a \<in> A" and "g a \<noteq> z"
+  assumes "F g A \<noteq> \<^bold>1"
+  obtains a where "a \<in> A" and "g a \<noteq> \<^bold>1"
 proof -
-  from assms have "\<exists>a\<in>A. g a \<noteq> z"
+  from assms have "\<exists>a\<in>A. g a \<noteq> \<^bold>1"
   proof (induct A rule: infinite_finite_induct)
     case (insert a A)
     then show ?case by simp (rule, simp)
@@ -180,7 +177,7 @@
 qed (auto dest: finite_UnionD intro: infinite)
 
 lemma distrib:
-  "F (\<lambda>x. g x * h x) A = F g A * F h A"
+  "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A"
   by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
 
 lemma Sigma:
@@ -197,14 +194,14 @@
 done
 
 lemma related:
-  assumes Re: "R 1 1"
-  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
+  assumes Re: "R \<^bold>1 \<^bold>1"
+  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)"
   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   shows "R (F h S) (F g S)"
   using fS by (rule finite_subset_induct) (insert assms, auto)
 
 lemma mono_neutral_cong_left:
-  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
+  assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = \<^bold>1"
   and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
 proof-
   have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast
@@ -216,16 +213,16 @@
 qed
 
 lemma mono_neutral_cong_right:
-  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
    \<Longrightarrow> F g T = F h S"
   by (auto intro!: mono_neutral_cong_left [symmetric])
 
 lemma mono_neutral_left:
-  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   by (blast intro: mono_neutral_cong_left)
 
 lemma mono_neutral_right:
-  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
+  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   by (blast intro!: mono_neutral_left [symmetric])
 
 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
@@ -275,10 +272,10 @@
 
 lemma reindex_nontrivial:
   assumes "finite A"
-  and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = 1"
+  and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = \<^bold>1"
   shows "F g (h ` A) = F (g \<circ> h) A"
 proof (subst reindex_bij_betw_not_neutral [symmetric])
-  show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
+  show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = \<^bold>1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = \<^bold>1})"
     using nz by (auto intro!: inj_onI simp: bij_betw_def)
 qed (insert \<open>finite A\<close>, auto)
 
@@ -307,11 +304,11 @@
 
 lemma delta:
   assumes fS: "finite S"
-  shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
+  shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
 proof-
-  let ?f = "(\<lambda>k. if k=a then b k else 1)"
+  let ?f = "(\<lambda>k. if k=a then b k else \<^bold>1)"
   { assume a: "a \<notin> S"
-    hence "\<forall>k\<in>S. ?f k = 1" by simp
+    hence "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
     hence ?thesis  using a by simp }
   moreover
   { assume a: "a \<in> S"
@@ -320,7 +317,7 @@
     have eq: "S = ?A \<union> ?B" using a by blast
     have dj: "?A \<inter> ?B = {}" by simp
     from fS have fAB: "finite ?A" "finite ?B" by auto
-    have "F ?f S = F ?f ?A * F ?f ?B"
+    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
       by simp
     then have ?thesis using a by simp }
@@ -329,14 +326,14 @@
 
 lemma delta':
   assumes fS: "finite S"
-  shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
+  shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   using delta [OF fS, of a b, symmetric] by (auto intro: cong)
 
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fA: "finite A"
   shows "F (\<lambda>x. if P x then h x else g x) A =
-    F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
+    F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})"
 proof -
   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
@@ -363,10 +360,10 @@
 
 lemma inter_restrict:
   assumes "finite A"
-  shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
+  shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A"
 proof -
-  let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
-  have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
+  let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1"
+  have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1"
    by simp
   moreover have "A \<inter> B \<subseteq> A" by blast
   ultimately have "F ?g (A \<inter> B) = F ?g A" using \<open>finite A\<close>
@@ -375,12 +372,12 @@
 qed
 
 lemma inter_filter:
-  "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else 1) A"
+  "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A"
   by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
 
 lemma Union_comp:
   assumes "\<forall>A \<in> B. finite A"
-    and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B  \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = 1"
+    and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B  \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = \<^bold>1"
   shows "F g (\<Union>B) = (F \<circ> F) g B"
 using assms proof (induct B rule: infinite_finite_induct)
   case (infinite A)
@@ -391,9 +388,9 @@
 next
   case (insert A B)
   then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
-    and "\<forall>x\<in>A \<inter> \<Union>B. g x = 1"
+    and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1"
     and H: "F g (\<Union>B) = (F o F) g B" by auto
-  then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
+  then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)"
     by (simp add: union_inter_neutral)
   with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
     by (simp add: H)
@@ -412,7 +409,7 @@
 lemma Plus:
   fixes A :: "'b set" and B :: "'c set"
   assumes fin: "finite A" "finite B"
-  shows "F g (A <+> B) = F (g \<circ> Inl) A * F (g \<circ> Inr) B"
+  shows "F g (A <+> B) = F (g \<circ> Inl) A \<^bold>* F (g \<circ> Inr) B"
 proof -
   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)"
@@ -427,7 +424,7 @@
 lemma same_carrier:
   assumes "finite C"
   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
-  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
 proof -
   from \<open>finite C\<close> subset have
@@ -437,12 +434,12 @@
   from subset have [simp]: "B - (C - B) = B" by auto
   from subset have "C = A \<union> (C - A)" by auto
   then have "F g C = F g (A \<union> (C - A))" by simp
-  also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
+  also have "\<dots> = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \<inter> (C - A))"
     using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
   finally have P: "F g C = F g A" using trivial by simp
   from subset have "C = B \<union> (C - B)" by auto
   then have "F h C = F h (B \<union> (C - B))" by simp
-  also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
+  also have "\<dots> = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \<inter> (C - B))"
     using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
   finally have Q: "F h C = F h B" using trivial by simp
   from P Q show ?thesis by simp
@@ -451,16 +448,13 @@
 lemma same_carrierI:
   assumes "finite C"
   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
-  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   assumes "F g C = F h C"
   shows "F g A = F h B"
   using assms same_carrier [of C A B] by simp
 
 end
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 
 subsection \<open>Generalized summation over a set\<close>
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Groups_List.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -6,26 +6,23 @@
 imports List
 begin
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
- 
 locale monoid_list = monoid
 begin
  
 definition F :: "'a list \<Rightarrow> 'a"
 where
-  eq_foldr [code]: "F xs = foldr f xs 1"
+  eq_foldr [code]: "F xs = foldr f xs \<^bold>1"
  
 lemma Nil [simp]:
-  "F [] = 1"
+  "F [] = \<^bold>1"
   by (simp add: eq_foldr)
  
 lemma Cons [simp]:
-  "F (x # xs) = x * F xs"
+  "F (x # xs) = x \<^bold>* F xs"
   by (simp add: eq_foldr)
  
 lemma append [simp]:
-  "F (xs @ ys) = F xs * F ys"
+  "F (xs @ ys) = F xs \<^bold>* F ys"
   by (induct xs) (simp_all add: assoc)
  
 end
@@ -52,9 +49,6 @@
 
 end
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 
 subsection \<open>List summation\<close>
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Lattices.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -16,17 +16,14 @@
   undesired effects may occur due to interpretation.
 \<close>
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
 locale semilattice = abel_semigroup +
-  assumes idem [simp]: "a * a = a"
+  assumes idem [simp]: "a \<^bold>* a = a"
 begin
 
-lemma left_idem [simp]: "a * (a * b) = a * b"
+lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
 by (simp add: assoc [symmetric])
 
-lemma right_idem [simp]: "(a * b) * b = a * b"
+lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
 by (simp add: assoc)
 
 end
@@ -34,109 +31,109 @@
 locale semilattice_neutr = semilattice + comm_monoid
 
 locale semilattice_order = semilattice +
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
-  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
-    and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
+  assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
+    and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
 begin
 
 lemma orderI:
-  "a = a * b \<Longrightarrow> a \<preceq> b"
+  "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
   by (simp add: order_iff)
 
 lemma orderE:
-  assumes "a \<preceq> b"
-  obtains "a = a * b"
+  assumes "a \<^bold>\<le> b"
+  obtains "a = a \<^bold>* b"
   using assms by (unfold order_iff)
 
 sublocale ordering less_eq less
 proof
   fix a b
-  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
     by (simp add: order_iff strict_order_iff)
 next
   fix a
-  show "a \<preceq> a"
+  show "a \<^bold>\<le> a"
     by (simp add: order_iff)
 next
   fix a b
-  assume "a \<preceq> b" "b \<preceq> a"
-  then have "a = a * b" "a * b = b"
+  assume "a \<^bold>\<le> b" "b \<^bold>\<le> a"
+  then have "a = a \<^bold>* b" "a \<^bold>* b = b"
     by (simp_all add: order_iff commute)
   then show "a = b" by simp
 next
   fix a b c
-  assume "a \<preceq> b" "b \<preceq> c"
-  then have "a = a * b" "b = b * c"
+  assume "a \<^bold>\<le> b" "b \<^bold>\<le> c"
+  then have "a = a \<^bold>* b" "b = b \<^bold>* c"
     by (simp_all add: order_iff commute)
-  then have "a = a * (b * c)"
+  then have "a = a \<^bold>* (b \<^bold>* c)"
     by simp
-  then have "a = (a * b) * c"
+  then have "a = (a \<^bold>* b) \<^bold>* c"
     by (simp add: assoc)
-  with \<open>a = a * b\<close> [symmetric] have "a = a * c" by simp
-  then show "a \<preceq> c" by (rule orderI)
+  with \<open>a = a \<^bold>* b\<close> [symmetric] have "a = a \<^bold>* c" by simp
+  then show "a \<^bold>\<le> c" by (rule orderI)
 qed
 
 lemma cobounded1 [simp]:
-  "a * b \<preceq> a"
+  "a \<^bold>* b \<^bold>\<le> a"
   by (simp add: order_iff commute)  
 
 lemma cobounded2 [simp]:
-  "a * b \<preceq> b"
+  "a \<^bold>* b \<^bold>\<le> b"
   by (simp add: order_iff)
 
 lemma boundedI:
-  assumes "a \<preceq> b" and "a \<preceq> c"
-  shows "a \<preceq> b * c"
+  assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
+  shows "a \<^bold>\<le> b \<^bold>* c"
 proof (rule orderI)
-  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
-  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
+  from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" by (auto elim!: orderE)
+  then show "a = a \<^bold>* (b \<^bold>* c)" by (simp add: assoc [symmetric])
 qed
 
 lemma boundedE:
-  assumes "a \<preceq> b * c"
-  obtains "a \<preceq> b" and "a \<preceq> c"
+  assumes "a \<^bold>\<le> b \<^bold>* c"
+  obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
   using assms by (blast intro: trans cobounded1 cobounded2)
 
 lemma bounded_iff [simp]:
-  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
+  "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
   by (blast intro: boundedI elim: boundedE)
 
 lemma strict_boundedE:
-  assumes "a \<prec> b * c"
-  obtains "a \<prec> b" and "a \<prec> c"
+  assumes "a \<^bold>< b \<^bold>* c"
+  obtains "a \<^bold>< b" and "a \<^bold>< c"
   using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
 
 lemma coboundedI1:
-  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+  "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   by (rule trans) auto
 
 lemma coboundedI2:
-  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
+  "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
   by (rule trans) auto
 
 lemma strict_coboundedI1:
-  "a \<prec> c \<Longrightarrow> a * b \<prec> c"
+  "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   using irrefl
     by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
 
 lemma strict_coboundedI2:
-  "b \<prec> c \<Longrightarrow> a * b \<prec> c"
+  "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
   using strict_coboundedI1 [of b c a] by (simp add: commute)
 
-lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
+lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
   by (blast intro: boundedI coboundedI1 coboundedI2)
 
-lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
+lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a"
   by (rule antisym) (auto simp add: refl)
 
-lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
+lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
   by (rule antisym) (auto simp add: refl)
 
-lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
+lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
   using order_iff by auto
 
-lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b"
+lemma absorb_iff2: "b \<^bold>\<le> a \<longleftrightarrow> a \<^bold>* b = b"
   using order_iff by (auto simp add: commute)
 
 end
@@ -144,14 +141,11 @@
 locale semilattice_neutr_order = semilattice_neutr + semilattice_order
 begin
 
-sublocale ordering_top less_eq less 1
+sublocale ordering_top less_eq less "\<^bold>1"
   by standard (simp add: order_iff)
 
 end
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Lattices_Big.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -11,10 +11,6 @@
 
 subsection \<open>Generic lattice operations over a set\<close>
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
-
 subsubsection \<open>Without neutral element\<close>
 
 locale semilattice_set = semilattice
@@ -48,20 +44,20 @@
 
 lemma insert_not_elem:
   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
-  shows "F (insert x A) = x * F A"
+  shows "F (insert x A) = x \<^bold>* F A"
 proof -
   from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
   with \<open>finite A\<close> and \<open>x \<notin> A\<close>
     have "finite (insert x B)" and "b \<notin> insert x B" by auto
-  then have "F (insert b (insert x B)) = x * F (insert b B)"
+  then have "F (insert b (insert x B)) = x \<^bold>* F (insert b B)"
     by (simp add: eq_fold)
   then show ?thesis by (simp add: * insert_commute)
 qed
 
 lemma in_idem:
   assumes "finite A" and "x \<in> A"
-  shows "x * F A = F A"
+  shows "x \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" by auto
   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
@@ -70,17 +66,17 @@
 
 lemma insert [simp]:
   assumes "finite A" and "A \<noteq> {}"
-  shows "F (insert x A) = x * F A"
+  shows "F (insert x A) = x \<^bold>* F A"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
 
 lemma union:
   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
-  shows "F (A \<union> B) = F A * F B"
+  shows "F (A \<union> B) = F A \<^bold>* F B"
   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
 
 lemma remove:
   assumes "finite A" and "x \<in> A"
-  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
+  shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
 proof -
   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   with assms show ?thesis by simp
@@ -88,19 +84,19 @@
 
 lemma insert_remove:
   assumes "finite A"
-  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
+  shows "F (insert x A) = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
 
 lemma subset:
   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
-  shows "F B * F A = F A"
+  shows "F B \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
 qed
 
 lemma closed:
-  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
   shows "F A \<in> A"
 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
   case singleton then show ?case by simp
@@ -109,17 +105,17 @@
 qed
 
 lemma hom_commute:
-  assumes hom: "\<And>x y. h (x * y) = h x * h y"
+  assumes hom: "\<And>x y. h (x \<^bold>* y) = h x \<^bold>* h y"
   and N: "finite N" "N \<noteq> {}"
   shows "h (F N) = F (h ` N)"
 using N proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
   case (insert n N)
-  then have "h (F (insert n N)) = h (n * F N)" by simp
-  also have "\<dots> = h n * h (F N)" by (rule hom)
+  then have "h (F (insert n N)) = h (n \<^bold>* F N)" by simp
+  also have "\<dots> = h n \<^bold>* h (F N)" by (rule hom)
   also have "h (F N) = F (h ` N)" by (rule insert)
-  also have "h n * \<dots> = F (insert (h n) (h ` N))"
+  also have "h n \<^bold>* \<dots> = F (insert (h n) (h ` N))"
     using insert by simp
   also have "insert (h n) (h ` N) = h ` insert n N" by simp
   finally show ?case .
@@ -135,25 +131,25 @@
 
 lemma bounded_iff:
   assumes "finite A" and "A \<noteq> {}"
-  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
+  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
 
 lemma boundedI:
   assumes "finite A"
   assumes "A \<noteq> {}"
-  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
-  shows "x \<preceq> F A"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
+  shows "x \<^bold>\<le> F A"
   using assms by (simp add: bounded_iff)
 
 lemma boundedE:
-  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
-  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
+  assumes "finite A" and "A \<noteq> {}" and "x \<^bold>\<le> F A"
+  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   using assms by (simp add: bounded_iff)
 
 lemma coboundedI:
   assumes "finite A"
     and "a \<in> A"
-  shows "F A \<preceq> a"
+  shows "F A \<^bold>\<le> a"
 proof -
   from assms have "A \<noteq> {}" by auto
   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
@@ -168,15 +164,15 @@
 
 lemma antimono:
   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
-  shows "F B \<preceq> F A"
+  shows "F B \<^bold>\<le> F A"
 proof (cases "A = B")
   case True then show ?thesis by (simp add: refl)
 next
   case False
   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   then have "F B = F (A \<union> (B - A))" by simp
-  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
-  also have "\<dots> \<preceq> F A" by simp
+  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
+  also have "\<dots> \<^bold>\<le> F A" by simp
   finally show ?thesis .
 qed
 
@@ -193,24 +189,24 @@
 
 definition F :: "'a set \<Rightarrow> 'a"
 where
-  eq_fold: "F A = Finite_Set.fold f 1 A"
+  eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
 
 lemma infinite [simp]:
-  "\<not> finite A \<Longrightarrow> F A = 1"
+  "\<not> finite A \<Longrightarrow> F A = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma empty [simp]:
-  "F {} = 1"
+  "F {} = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma insert [simp]:
   assumes "finite A"
-  shows "F (insert x A) = x * F A"
+  shows "F (insert x A) = x \<^bold>* F A"
   using assms by (simp add: eq_fold)
 
 lemma in_idem:
   assumes "finite A" and "x \<in> A"
-  shows "x * F A = F A"
+  shows "x \<^bold>* F A = F A"
 proof -
   from assms have "A \<noteq> {}" by auto
   with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
@@ -219,12 +215,12 @@
 
 lemma union:
   assumes "finite A" and "finite B"
-  shows "F (A \<union> B) = F A * F B"
+  shows "F (A \<union> B) = F A \<^bold>* F B"
   using assms by (induct A) (simp_all add: ac_simps)
 
 lemma remove:
   assumes "finite A" and "x \<in> A"
-  shows "F A = x * F (A - {x})"
+  shows "F A = x \<^bold>* F (A - {x})"
 proof -
   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   with assms show ?thesis by simp
@@ -232,19 +228,19 @@
 
 lemma insert_remove:
   assumes "finite A"
-  shows "F (insert x A) = x * F (A - {x})"
+  shows "F (insert x A) = x \<^bold>* F (A - {x})"
   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
 
 lemma subset:
   assumes "finite A" and "B \<subseteq> A"
-  shows "F B * F A = F A"
+  shows "F B \<^bold>* F A = F A"
 proof -
   from assms have "finite B" by (auto dest: finite_subset)
   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
 qed
 
 lemma closed:
-  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
+  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}"
   shows "F A \<in> A"
 using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct)
   case singleton then show ?case by simp
@@ -259,24 +255,24 @@
 
 lemma bounded_iff:
   assumes "finite A"
-  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
+  shows "x \<^bold>\<le> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<^bold>\<le> a)"
   using assms by (induct A) (simp_all add: bounded_iff)
 
 lemma boundedI:
   assumes "finite A"
-  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
-  shows "x \<preceq> F A"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
+  shows "x \<^bold>\<le> F A"
   using assms by (simp add: bounded_iff)
 
 lemma boundedE:
-  assumes "finite A" and "x \<preceq> F A"
-  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
+  assumes "finite A" and "x \<^bold>\<le> F A"
+  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<^bold>\<le> a"
   using assms by (simp add: bounded_iff)
 
 lemma coboundedI:
   assumes "finite A"
     and "a \<in> A"
-  shows "F A \<preceq> a"
+  shows "F A \<^bold>\<le> a"
 proof -
   from assms have "A \<noteq> {}" by auto
   from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> show ?thesis
@@ -291,23 +287,20 @@
 
 lemma antimono:
   assumes "A \<subseteq> B" and "finite B"
-  shows "F B \<preceq> F A"
+  shows "F B \<^bold>\<le> F A"
 proof (cases "A = B")
   case True then show ?thesis by (simp add: refl)
 next
   case False
   have B: "B = A \<union> (B - A)" using \<open>A \<subseteq> B\<close> by blast
   then have "F B = F (A \<union> (B - A))" by simp
-  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
-  also have "\<dots> \<preceq> F A" by simp
+  also have "\<dots> = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
+  also have "\<dots> \<^bold>\<le> F A" by simp
   finally show ?thesis .
 qed
 
 end
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 
 subsection \<open>Lattice operations on finite sets\<close>
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -9,21 +9,18 @@
 
 subsection \<open>Abstract product\<close>
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
 locale comm_monoid_fun = comm_monoid
 begin
 
 definition G :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
 where
-  expand_set: "G g = comm_monoid_set.F f 1 g {a. g a \<noteq> 1}"
+  expand_set: "G g = comm_monoid_set.F f \<^bold>1 g {a. g a \<noteq> \<^bold>1}"
 
-interpretation F: comm_monoid_set f 1
+interpretation F: comm_monoid_set f "\<^bold>1"
   ..
 
 lemma expand_superset:
-  assumes "finite A" and "{a. g a \<noteq> 1} \<subseteq> A"
+  assumes "finite A" and "{a. g a \<noteq> \<^bold>1} \<subseteq> A"
   shows "G g = F.F g A"
   apply (simp add: expand_set)
   apply (rule F.same_carrierI [of A])
@@ -32,7 +29,7 @@
 
 lemma conditionalize:
   assumes "finite A"
-  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else 1)"
+  shows "F.F g A = G (\<lambda>a. if a \<in> A then g a else \<^bold>1)"
   using assms
   apply (simp add: expand_set)
   apply (rule F.same_carrierI [of A])
@@ -40,29 +37,29 @@
   done
 
 lemma neutral [simp]:
-  "G (\<lambda>a. 1) = 1"
+  "G (\<lambda>a. \<^bold>1) = \<^bold>1"
   by (simp add: expand_set)
 
 lemma update [simp]:
-  assumes "finite {a. g a \<noteq> 1}"
-  assumes "g a = 1"
-  shows "G (g(a := b)) = b * G g"
-proof (cases "b = 1")
-  case True with \<open>g a = 1\<close> show ?thesis
+  assumes "finite {a. g a \<noteq> \<^bold>1}"
+  assumes "g a = \<^bold>1"
+  shows "G (g(a := b)) = b \<^bold>* G g"
+proof (cases "b = \<^bold>1")
+  case True with \<open>g a = \<^bold>1\<close> show ?thesis
     by (simp add: expand_set) (rule F.cong, auto)
 next
   case False
-  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
+  moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> \<^bold>1} = insert a {a. g a \<noteq> \<^bold>1}"
     by auto
-  moreover from \<open>g a = 1\<close> have "a \<notin> {a. g a \<noteq> 1}"
+  moreover from \<open>g a = \<^bold>1\<close> have "a \<notin> {a. g a \<noteq> \<^bold>1}"
     by simp
-  moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> 1} = F.F g {a. g a \<noteq> 1}"
-    by (rule F.cong) (auto simp add: \<open>g a = 1\<close>)
-  ultimately show ?thesis using \<open>finite {a. g a \<noteq> 1}\<close> by (simp add: expand_set)
+  moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> \<^bold>1} = F.F g {a. g a \<noteq> \<^bold>1}"
+    by (rule F.cong) (auto simp add: \<open>g a = \<^bold>1\<close>)
+  ultimately show ?thesis using \<open>finite {a. g a \<noteq> \<^bold>1}\<close> by (simp add: expand_set)
 qed
 
 lemma infinite [simp]:
-  "\<not> finite {a. g a \<noteq> 1} \<Longrightarrow> G g = 1"
+  "\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
   by (simp add: expand_set)
 
 lemma cong:
@@ -76,8 +73,8 @@
   using assms by (fact cong)
 
 lemma not_neutral_obtains_not_neutral:
-  assumes "G g \<noteq> 1"
-  obtains a where "g a \<noteq> 1"
+  assumes "G g \<noteq> \<^bold>1"
+  obtains a where "g a \<noteq> \<^bold>1"
   using assms by (auto elim: F.not_neutral_contains_not_neutral simp add: expand_set)
 
 lemma reindex_cong:
@@ -87,59 +84,59 @@
 proof -
   from assms have unfold: "h = g \<circ> l" by simp
   from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
-  then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
-  moreover from \<open>bij l\<close> have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
+  then have "inj_on l {a. h a \<noteq> \<^bold>1}" by (rule subset_inj_on) simp
+  moreover from \<open>bij l\<close> have "{a. g a \<noteq> \<^bold>1} = l ` {a. h a \<noteq> \<^bold>1}"
     by (auto simp add: image_Collect unfold elim: bij_pointE)
-  moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
+  moreover have "\<And>x. x \<in> {a. h a \<noteq> \<^bold>1} \<Longrightarrow> g (l x) = h x"
     by (simp add: unfold)
-  ultimately have "F.F g {a. g a \<noteq> 1} = F.F h {a. h a \<noteq> 1}"
+  ultimately have "F.F g {a. g a \<noteq> \<^bold>1} = F.F h {a. h a \<noteq> \<^bold>1}"
     by (rule F.reindex_cong)
   then show ?thesis by (simp add: expand_set)
 qed
 
 lemma distrib:
-  assumes "finite {a. g a \<noteq> 1}" and "finite {a. h a \<noteq> 1}"
-  shows "G (\<lambda>a. g a * h a) = G g * G h"
+  assumes "finite {a. g a \<noteq> \<^bold>1}" and "finite {a. h a \<noteq> \<^bold>1}"
+  shows "G (\<lambda>a. g a \<^bold>* h a) = G g \<^bold>* G h"
 proof -
-  from assms have "finite ({a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1})" by simp
-  moreover have "{a. g a * h a \<noteq> 1} \<subseteq> {a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"
+  from assms have "finite ({a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1})" by simp
+  moreover have "{a. g a \<^bold>* h a \<noteq> \<^bold>1} \<subseteq> {a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"
     by auto (drule sym, simp)
   ultimately show ?thesis
     using assms
-    by (simp add: expand_superset [of "{a. g a \<noteq> 1} \<union> {a. h a \<noteq> 1}"] F.distrib)
+    by (simp add: expand_superset [of "{a. g a \<noteq> \<^bold>1} \<union> {a. h a \<noteq> \<^bold>1}"] F.distrib)
 qed
 
 lemma commute:
   assumes "finite C"
-  assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
+  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
 proof -
   from \<open>finite C\<close> subset
-    have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
+    have "finite ({a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1})"
     by (rule rev_finite_subset)
   then have fins:
-    "finite {b. \<exists>a. g a b \<noteq> 1}" "finite {a. \<exists>b. g a b \<noteq> 1}"
+    "finite {b. \<exists>a. g a b \<noteq> \<^bold>1}" "finite {a. \<exists>b. g a b \<noteq> \<^bold>1}"
     by (auto simp add: finite_cartesian_product_iff)
-  have subsets: "\<And>a. {b. g a b \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
-    "\<And>b. {a. g a b \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
-    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {a. \<exists>b. g a b \<noteq> 1}"
-    "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> 1} \<noteq> 1} \<subseteq> {b. \<exists>a. g a b \<noteq> 1}"
+  have subsets: "\<And>a. {b. g a b \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
+    "\<And>b. {a. g a b \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
+    "{a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {a. \<exists>b. g a b \<noteq> \<^bold>1}"
+    "{a. F.F (\<lambda>aa. g aa a) {a. \<exists>b. g a b \<noteq> \<^bold>1} \<noteq> \<^bold>1} \<subseteq> {b. \<exists>a. g a b \<noteq> \<^bold>1}"
     by (auto elim: F.not_neutral_contains_not_neutral)
   from F.commute have
-    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1} =
-      F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1}) {b. \<exists>a. g a b \<noteq> 1}" .
-  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) =
-    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> 1})"
-    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
-      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
+    "F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1} =
+      F.F (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1}) {b. \<exists>a. g a b \<noteq> \<^bold>1}" .
+  with subsets fins have "G (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) =
+    G (\<lambda>b. F.F (\<lambda>a. g a b) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
+    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
+      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
   with subsets fins show ?thesis
-    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> 1}"]
-      expand_superset [of "{a. \<exists>b. g a b \<noteq> 1}"])
+    by (auto simp add: expand_superset [of "{b. \<exists>a. g a b \<noteq> \<^bold>1}"]
+      expand_superset [of "{a. \<exists>b. g a b \<noteq> \<^bold>1}"])
 qed
 
 lemma cartesian_product:
   assumes "finite C"
-  assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
+  assumes subset: "{a. \<exists>b. g a b \<noteq> \<^bold>1} \<times> {b. \<exists>a. g a b \<noteq> \<^bold>1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
   shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
 proof -
   from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
@@ -147,7 +144,7 @@
   from fin_prod have "finite ?A" and "finite ?B"
     by (auto simp add: finite_cartesian_product_iff)
   have *: "G (\<lambda>a. G (g a)) =
-    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
+    (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> \<^bold>1}) {a. \<exists>b. g a b \<noteq> \<^bold>1})"
     apply (subst expand_superset [of "?B"])
     apply (rule \<open>finite ?B\<close>)
     apply auto
@@ -157,9 +154,9 @@
     apply (erule F.not_neutral_contains_not_neutral)
     apply auto
     done
-  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> ?A \<times> ?B"
+  have "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> ?A \<times> ?B"
     by auto
-  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> 1} \<subseteq> C"
+  with subset have **: "{p. (case p of (a, b) \<Rightarrow> g a b) \<noteq> \<^bold>1} \<subseteq> C"
     by blast
   show ?thesis
     apply (simp add: *)
@@ -176,12 +173,12 @@
 
 lemma cartesian_product2:
   assumes fin: "finite D"
-  assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> 1} \<times> {c. \<exists>a b. g a b c \<noteq> 1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
+  assumes subset: "{(a, b). \<exists>c. g a b c \<noteq> \<^bold>1} \<times> {c. \<exists>a b. g a b c \<noteq> \<^bold>1} \<subseteq> D" (is "?AB \<times> ?C \<subseteq> D")
   shows "G (\<lambda>(a, b). G (g a b)) = G (\<lambda>(a, b, c). g a b c)"
 proof -
   have bij: "bij (\<lambda>(a, b, c). ((a, b), c))"
     by (auto intro!: bijI injI simp add: image_def)
-  have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> 1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> 1} \<subseteq> D"
+  have "{p. \<exists>c. g (fst p) (snd p) c \<noteq> \<^bold>1} \<times> {c. \<exists>p. g (fst p) (snd p) c \<noteq> \<^bold>1} \<subseteq> D"
     by auto (insert subset, blast)
   with fin have "G (\<lambda>p. G (g (fst p) (snd p))) = G (\<lambda>(p, c). g (fst p) (snd p) c)"
     by (rule cartesian_product)
@@ -193,27 +190,24 @@
 qed
 
 lemma delta [simp]:
-  "G (\<lambda>b. if b = a then g b else 1) = g a"
+  "G (\<lambda>b. if b = a then g b else \<^bold>1) = g a"
 proof -
-  have "{b. (if b = a then g b else 1) \<noteq> 1} \<subseteq> {a}" by auto
+  have "{b. (if b = a then g b else \<^bold>1) \<noteq> \<^bold>1} \<subseteq> {a}" by auto
   then show ?thesis by (simp add: expand_superset [of "{a}"])
 qed
 
 lemma delta' [simp]:
-  "G (\<lambda>b. if a = b then g b else 1) = g a"
+  "G (\<lambda>b. if a = b then g b else \<^bold>1) = g a"
 proof -
-  have "(\<lambda>b. if a = b then g b else 1) = (\<lambda>b. if b = a then g b else 1)"
+  have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
     by (simp add: fun_eq_iff)
-  then have "G (\<lambda>b. if a = b then g b else 1) = G (\<lambda>b. if b = a then g b else 1)"
+  then have "G (\<lambda>b. if a = b then g b else \<^bold>1) = G (\<lambda>b. if b = a then g b else \<^bold>1)"
     by (simp cong del: strong_cong)
   then show ?thesis by simp
 qed
 
 end
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 
 subsection \<open>Concrete sum\<close>
 
@@ -339,4 +333,3 @@
 qed
 
 end
-
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -1562,16 +1562,13 @@
 
 subsection \<open>Big operators\<close>
 
-no_notation times (infixl "*" 70)
-no_notation Groups.one ("1")
-
 locale comm_monoid_mset = comm_monoid
 begin
 
 definition F :: "'a multiset \<Rightarrow> 'a"
-  where eq_fold: "F M = fold_mset f 1 M"
-
-lemma empty [simp]: "F {#} = 1"
+  where eq_fold: "F M = fold_mset f \<^bold>1 M"
+
+lemma empty [simp]: "F {#} = \<^bold>1"
   by (simp add: eq_fold)
 
 lemma singleton [simp]: "F {#x#} = x"
@@ -1581,7 +1578,7 @@
   show ?thesis by (simp add: eq_fold)
 qed
 
-lemma union [simp]: "F (M + N) = F M * F N"
+lemma union [simp]: "F (M + N) = F M \<^bold>* F N"
 proof -
   interpret comp_fun_commute f
     by standard (simp add: fun_eq_iff left_commute)
@@ -1599,9 +1596,6 @@
 lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   by (induct NN) auto
 
-notation times (infixl "*" 70)
-notation Groups.one ("1")
-
 context comm_monoid_add
 begin
 
diff -r 26134a00d060 -r 9ac558ab0906 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Jun 11 17:40:52 2016 +0200
+++ b/src/HOL/Orderings.thy	Sat Jun 11 16:22:42 2016 +0200
@@ -15,71 +15,71 @@
 subsection \<open>Abstract ordering\<close>
 
 locale ordering =
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
-   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
-  assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
-  assumes refl: "a \<preceq> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
-    and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
-    and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
+   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
+  assumes strict_iff_order: "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
+  assumes refl: "a \<^bold>\<le> a" \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
+    and antisym: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> a \<Longrightarrow> a = b"
+    and trans: "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>\<le> c"
 begin
 
 lemma strict_implies_order:
-  "a \<prec> b \<Longrightarrow> a \<preceq> b"
+  "a \<^bold>< b \<Longrightarrow> a \<^bold>\<le> b"
   by (simp add: strict_iff_order)
 
 lemma strict_implies_not_eq:
-  "a \<prec> b \<Longrightarrow> a \<noteq> b"
+  "a \<^bold>< b \<Longrightarrow> a \<noteq> b"
   by (simp add: strict_iff_order)
 
 lemma not_eq_order_implies_strict:
-  "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
+  "a \<noteq> b \<Longrightarrow> a \<^bold>\<le> b \<Longrightarrow> a \<^bold>< b"
   by (simp add: strict_iff_order)
 
 lemma order_iff_strict:
-  "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
+  "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
   by (auto simp add: strict_iff_order refl)
 
 lemma irrefl: \<comment> \<open>not \<open>iff\<close>: makes problems due to multiple (dual) interpretations\<close>
-  "\<not> a \<prec> a"
+  "\<not> a \<^bold>< a"
   by (simp add: strict_iff_order)
 
 lemma asym:
-  "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
+  "a \<^bold>< b \<Longrightarrow> b \<^bold>< a \<Longrightarrow> False"
   by (auto simp add: strict_iff_order intro: antisym)
 
 lemma strict_trans1:
-  "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+  "a \<^bold>\<le> b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
   by (auto simp add: strict_iff_order intro: trans antisym)
 
 lemma strict_trans2:
-  "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
+  "a \<^bold>< b \<Longrightarrow> b \<^bold>\<le> c \<Longrightarrow> a \<^bold>< c"
   by (auto simp add: strict_iff_order intro: trans antisym)
 
 lemma strict_trans:
-  "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
+  "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
   by (auto intro: strict_trans1 strict_implies_order)
 
 end
 
 locale ordering_top = ordering +
-  fixes top :: "'a"
-  assumes extremum [simp]: "a \<preceq> top"
+  fixes top :: "'a"  ("\<^bold>\<top>")
+  assumes extremum [simp]: "a \<^bold>\<le> \<^bold>\<top>"
 begin
 
 lemma extremum_uniqueI:
-  "top \<preceq> a \<Longrightarrow> a = top"
+  "\<^bold>\<top> \<^bold>\<le> a \<Longrightarrow> a = \<^bold>\<top>"
   by (rule antisym) auto
 
 lemma extremum_unique:
-  "top \<preceq> a \<longleftrightarrow> a = top"
+  "\<^bold>\<top> \<^bold>\<le> a \<longleftrightarrow> a = \<^bold>\<top>"
   by (auto intro: antisym)
 
 lemma extremum_strict [simp]:
-  "\<not> (top \<prec> a)"
+  "\<not> (\<^bold>\<top> \<^bold>< a)"
   using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
 
 lemma not_eq_extremum:
-  "a \<noteq> top \<longleftrightarrow> a \<prec> top"
+  "a \<noteq> \<^bold>\<top> \<longleftrightarrow> a \<^bold>< \<^bold>\<top>"
   by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
 
 end