--- 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
--- 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]
--- 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)