diff -r de51a86fc903 -r cc97b347b301 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Groups.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -158,6 +158,8 @@
 
 end
 
+hide_fact add_assoc
+
 class ab_semigroup_add = semigroup_add +
   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
 begin
@@ -165,13 +167,15 @@
 sublocale add!: abel_semigroup plus
   by default (fact add_commute)
 
-lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
+declare add.left_commute [algebra_simps, field_simps]
 
-theorems add_ac = add_assoc add_commute add_left_commute
+theorems add_ac = add.assoc add.commute add.left_commute
 
 end
 
-theorems add_ac = add_assoc add_commute add_left_commute
+hide_fact add_commute
+
+theorems add_ac = add.assoc add.commute add.left_commute
 
 class semigroup_mult = times +
   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
@@ -182,6 +186,8 @@
 
 end
 
+hide_fact mult_assoc
+
 class ab_semigroup_mult = semigroup_mult +
   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
 begin
@@ -189,13 +195,15 @@
 sublocale mult!: abel_semigroup times
   by default (fact mult_commute)
 
-lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
+declare mult.left_commute [algebra_simps, field_simps]
 
-theorems mult_ac = mult_assoc mult_commute mult_left_commute
+theorems mult_ac = mult.assoc mult.commute mult.left_commute
 
 end
 
-theorems mult_ac = mult_assoc mult_commute mult_left_commute
+hide_fact mult_commute
+
+theorems mult_ac = mult.assoc mult.commute mult.left_commute
 
 class monoid_add = zero + semigroup_add +
   assumes add_0_left: "0 + a = a"
@@ -325,7 +333,7 @@
 next
   fix a b c :: 'a
   assume "b + a = c + a"
-  then have "a + b = a + c" by (simp only: add_commute)
+  then have "a + b = a + c" by (simp only: add.commute)
   then show "b = c" by (rule add_imp_eq)
 qed
 
@@ -349,7 +357,7 @@
   assumes "a + b = 0" shows "- a = b"
 proof -
   have "- a = - a + (a + b)" using assms by simp
-  also have "\<dots> = b" by (simp add: add_assoc [symmetric])
+  also have "\<dots> = b" by (simp add: add.assoc [symmetric])
   finally show ?thesis .
 qed
 
@@ -381,36 +389,36 @@
   fix a b c :: 'a
   assume "a + b = a + c"
   then have "- a + a + b = - a + a + c"
-    unfolding add_assoc by simp
+    unfolding add.assoc by simp
   then show "b = c" by simp
 next
   fix a b c :: 'a
   assume "b + a = c + a"
   then have "b + a + - a = c + a  + - a" by simp
-  then show "b = c" unfolding add_assoc by simp
+  then show "b = c" unfolding add.assoc by simp
 qed
 
 lemma minus_add_cancel [simp]:
   "- a + (a + b) = b"
-  by (simp add: add_assoc [symmetric])
+  by (simp add: add.assoc [symmetric])
 
 lemma add_minus_cancel [simp]:
   "a + (- a + b) = b"
-  by (simp add: add_assoc [symmetric])
+  by (simp add: add.assoc [symmetric])
 
 lemma diff_add_cancel [simp]:
   "a - b + b = a"
-  by (simp only: diff_conv_add_uminus add_assoc) simp
+  by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma add_diff_cancel [simp]:
   "a + b - b = a"
-  by (simp only: diff_conv_add_uminus add_assoc) simp
+  by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma minus_add:
   "- (a + b) = - b + - a"
 proof -
   have "(a + b) + (- b + - a) = 0"
-    by (simp only: add_assoc add_minus_cancel) simp
+    by (simp only: add.assoc add_minus_cancel) simp
   then show "- (a + b) = - b + - a"
     by (rule minus_unique)
 qed
@@ -419,7 +427,7 @@
   "a - b = 0 \<longleftrightarrow> a = b"
 proof
   assume "a - b = 0"
-  have "a = (a - b) + b" by (simp add: add_assoc)
+  have "a = (a - b) + b" by (simp add: add.assoc)
   also have "\<dots> = b" using `a - b = 0` by simp
   finally show "a = b" .
 next
@@ -484,7 +492,7 @@
 next
   assume "a + b = 0"
   moreover have "a + (b + - b) = (a + b) + - b"
-    by (simp only: add_assoc)
+    by (simp only: add.assoc)
   ultimately show "a = - b" by simp
 qed
 
@@ -502,15 +510,15 @@
 
 lemma minus_diff_eq [simp]:
   "- (a - b) = b - a"
-  by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add_assoc minus_add_cancel) simp
+  by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp
 
 lemma add_diff_eq [algebra_simps, field_simps]:
   "a + (b - c) = (a + b) - c"
-  by (simp only: diff_conv_add_uminus add_assoc)
+  by (simp only: diff_conv_add_uminus add.assoc)
 
 lemma diff_add_eq_diff_diff_swap:
   "a - (b + c) = a - c - b"
-  by (simp only: diff_conv_add_uminus add_assoc minus_add)
+  by (simp only: diff_conv_add_uminus add.assoc minus_add)
 
 lemma diff_eq_eq [algebra_simps, field_simps]:
   "a - b = c \<longleftrightarrow> a = c + b"
@@ -522,7 +530,7 @@
 
 lemma diff_diff_eq2 [algebra_simps, field_simps]:
   "a - (b - c) = (a + c) - b"
-  by (simp only: diff_conv_add_uminus add_assoc) simp
+  by (simp only: diff_conv_add_uminus add.assoc) simp
 
 lemma diff_eq_diff_eq:
   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
@@ -543,13 +551,13 @@
   fix a b c :: 'a
   assume "a + b = a + c"
   then have "- a + a + b = - a + a + c"
-    by (simp only: add_assoc)
+    by (simp only: add.assoc)
   then show "b = c" by simp
 qed
 
 lemma uminus_add_conv_diff [simp]:
   "- a + b = b - a"
-  by (simp add: add_commute)
+  by (simp add: add.commute)
 
 lemma minus_add_distrib [simp]:
   "- (a + b) = - a + - b"
@@ -595,13 +603,13 @@
 
 lemma add_right_mono:
   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
-by (simp add: add_commute [of _ c] add_left_mono)
+by (simp add: add.commute [of _ c] add_left_mono)
 
 text {* non-strict, in both arguments *}
 lemma add_mono:
   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   apply (erule add_right_mono [THEN order_trans])
-  apply (simp add: add_commute add_left_mono)
+  apply (simp add: add.commute add_left_mono)
   done
 
 end
@@ -616,7 +624,7 @@
 
 lemma add_strict_right_mono:
   "a < b \<Longrightarrow> a + c < b + c"
-by (simp add: add_commute [of _ c] add_strict_left_mono)
+by (simp add: add.commute [of _ c] add_strict_left_mono)
 
 text{*Strict monotonicity in both arguments*}
 lemma add_strict_mono:
@@ -665,7 +673,7 @@
 lemma add_less_imp_less_right:
   "a + c < b + c \<Longrightarrow> a < b"
 apply (rule add_less_imp_less_left [of c])
-apply (simp add: add_commute)  
+apply (simp add: add.commute)  
 done
 
 lemma add_less_cancel_left [simp]:
@@ -682,7 +690,7 @@
 
 lemma add_le_cancel_right [simp]:
   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
-  by (simp add: add_commute [of a c] add_commute [of b c])
+  by (simp add: add.commute [of a c] add.commute [of b c])
 
 lemma add_le_imp_le_right:
   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
@@ -721,45 +729,45 @@
 
 lemma add_diff_assoc:
   "c + (b - a) = c + b - a"
-  using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
+  using `a \<le> b` by (auto simp add: le_iff_add add.left_commute [of c])
 
 lemma add_diff_assoc2:
   "b - a + c = b + c - a"
-  using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
+  using `a \<le> b` by (auto simp add: le_iff_add add.assoc)
 
 lemma diff_add_assoc:
   "c + b - a = c + (b - a)"
-  using `a \<le> b` by (simp add: add_commute add_diff_assoc)
+  using `a \<le> b` by (simp add: add.commute add_diff_assoc)
 
 lemma diff_add_assoc2:
   "b + c - a = b - a + c"
-  using `a \<le> b`by (simp add: add_commute add_diff_assoc)
+  using `a \<le> b`by (simp add: add.commute add_diff_assoc)
 
 lemma diff_diff_right:
   "c - (b - a) = c + a - b"
-  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
+  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
 
 lemma diff_add:
   "b - a + a = b"
-  by (simp add: add_commute add_diff_inverse)
+  by (simp add: add.commute add_diff_inverse)
 
 lemma le_add_diff:
   "c \<le> b + c - a"
-  by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
+  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
 
 lemma le_imp_diff_is_add:
   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
-  by (auto simp add: add_commute add_diff_inverse)
+  by (auto simp add: add.commute add_diff_inverse)
 
 lemma le_diff_conv2:
   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?P
   then have "c + a \<le> b - a + a" by (rule add_right_mono)
-  then show ?Q by (simp add: add_diff_inverse add_commute)
+  then show ?Q by (simp add: add_diff_inverse add.commute)
 next
   assume ?Q
-  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
+  then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
   then show ?P by simp
 qed
 
@@ -860,7 +868,7 @@
 
 lemma add_increasing2:
   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
-  by (simp add: add_increasing add_commute [of a])
+  by (simp add: add_increasing add.commute [of a])
 
 lemma add_strict_increasing:
   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
@@ -883,7 +891,7 @@
   fix a b c :: 'a
   assume "c + a \<le> c + b"
   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
-  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
+  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
   thus "a \<le> b" by simp
 qed