# HG changeset patch
# Parent  3e20defb1e3cb9d3a774394c67e62741fa96f8b3
removed dangerous simp rule: prime computations can be excessively long

diff -r 3e20defb1e3c -r c4c943d25be5 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Dec 08 15:11:20 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Dec 08 17:55:24 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)")