# HG changeset patch
# User haftmann
# Date 1424359973 -3600
# Node ID 35da1bbf234ee84903a3b73e30103f1d6549e48c
# Parent  5d9f0ace9af0051f5119e4182bd6dda5cec394e2
more canonical order of subscriptions avoids superfluous facts

diff -r 5d9f0ace9af0 -r 35da1bbf234e src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Feb 19 17:01:46 2015 +0000
+++ b/src/HOL/Groups.thy	Thu Feb 19 16:32:53 2015 +0100
@@ -200,11 +200,11 @@
   assumes add_0: "0 + a = a"
 begin
 
-sublocale add!: comm_monoid plus 0
-  by default (insert add_0, simp add: ac_simps)
+subclass monoid_add
+  by default (simp_all add: add_0 add.commute [of _ 0])
 
-subclass monoid_add
-  by default (fact add.left_neutral add.right_neutral)+
+sublocale add!: comm_monoid plus 0
+  by default (simp add: ac_simps)
 
 end
 
@@ -225,11 +225,11 @@
   assumes mult_1: "1 * a = a"
 begin
 
-sublocale mult!: comm_monoid times 1
-  by default (insert mult_1, simp add: ac_simps)
+subclass monoid_mult
+  by default (simp_all add: mult_1 mult.commute [of _ 1])
 
-subclass monoid_mult
-  by default (fact mult.left_neutral mult.right_neutral)+
+sublocale mult!: comm_monoid times 1
+  by default (simp add: ac_simps)
 
 end
 
diff -r 5d9f0ace9af0 -r 35da1bbf234e src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Thu Feb 19 17:01:46 2015 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Feb 19 16:32:53 2015 +0100
@@ -111,7 +111,7 @@
     assume e: "y \<le> (int p - 1) div 2"
     from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
     have "[x = y](mod p)"
-      by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
+      by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
                 cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
         order_le_less_trans [of x "(int p - 1) div 2" p]
diff -r 5d9f0ace9af0 -r 35da1bbf234e src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Feb 19 17:01:46 2015 +0000
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Feb 19 16:32:53 2015 +0100
@@ -130,7 +130,7 @@
 sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
 proof
   have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
-    by (metis comm_monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
+    by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
   from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]
     show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"
     by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)