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