--- a/src/HOL/Number_Theory/Factorial_Ring.thy Tue Dec 20 15:39:13 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy Wed Dec 21 21:26:25 2016 +0100
@@ -451,7 +451,7 @@
lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
by (intro prime_elem_dvd_multD) simp_all
-lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
by (auto dest: prime_dvd_multD)
lemma prime_dvd_power:
@@ -1640,7 +1640,6 @@
(insert nz False, auto simp: Gcd_factorial_eq_0_iff)
qed (simp_all add: Gcd_factorial_def)
-
lemma normalize_Lcm_factorial:
"normalize (Lcm_factorial A) = Lcm_factorial A"
proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
--- a/src/HOL/Number_Theory/Gauss.thy Tue Dec 20 15:39:13 2016 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Wed Dec 21 21:26:25 2016 +0100
@@ -12,12 +12,12 @@
lemma cong_prime_prod_zero_nat:
fixes a::nat
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
- by (auto simp add: cong_altdef_nat)
+ by (auto simp add: cong_altdef_nat prime_dvd_mult_iff)
lemma cong_prime_prod_zero_int:
fixes a::int
shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
- by (auto simp add: cong_altdef_int)
+ by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
locale GAUSS =