src/HOL/Groups.thy
 changeset 63290 9ac558ab0906 parent 63145 703edebd1d92 child 63325 1086d56cde86
```     1.1 --- a/src/HOL/Groups.thy	Sat Jun 11 17:40:52 2016 +0200
1.2 +++ b/src/HOL/Groups.thy	Sat Jun 11 16:22:42 2016 +0200
1.3 @@ -42,17 +42,17 @@
1.4  \<close>
1.5
1.6  locale semigroup =
1.7 -  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
1.8 -  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
1.9 +  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
1.10 +  assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
1.11
1.12  locale abel_semigroup = semigroup +
1.13 -  assumes commute [ac_simps]: "a * b = b * a"
1.14 +  assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
1.15  begin
1.16
1.17  lemma left_commute [ac_simps]:
1.18 -  "b * (a * c) = a * (b * c)"
1.19 +  "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
1.20  proof -
1.21 -  have "(b * a) * c = (a * b) * c"
1.22 +  have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
1.23      by (simp only: commute)
1.24    then show ?thesis
1.25      by (simp only: assoc)
1.26 @@ -61,13 +61,13 @@
1.27  end
1.28
1.29  locale monoid = semigroup +
1.30 -  fixes z :: 'a ("1")
1.31 -  assumes left_neutral [simp]: "1 * a = a"
1.32 -  assumes right_neutral [simp]: "a * 1 = a"
1.33 +  fixes z :: 'a ("\<^bold>1")
1.34 +  assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
1.35 +  assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
1.36
1.37  locale comm_monoid = abel_semigroup +
1.38 -  fixes z :: 'a ("1")
1.39 -  assumes comm_neutral: "a * 1 = a"
1.40 +  fixes z :: 'a ("\<^bold>1")
1.41 +  assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
1.42  begin
1.43
1.44  sublocale monoid
```