src/HOL/Library/Polynomial_Factorial.thy
 changeset 63905 1c3dcb5fe6cb parent 63830 2ea3725a34bd child 63950 cdc1e59aa513
```     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 16 12:30:55 2016 +0200
1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 16 12:30:55 2016 +0200
1.3 @@ -794,7 +794,7 @@
1.4  lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
1.5  proof -
1.6    have "Lcm_coeff_denoms (fract_poly p) = 1"
1.7 -    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
1.8 +    by (auto simp: set_coeffs_map_poly)
1.9    hence "fract_content (fract_poly p) =
1.10             to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
1.11      by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
1.12 @@ -1063,7 +1063,7 @@
1.13    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
1.14    have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1
1.15               normalize_field_poly unit_factor_field_poly" ..
1.16 -  from field_poly.in_prime_factorization_imp_prime[of p x] assms
1.17 +  from field_poly.in_prime_factors_imp_prime [of p x] assms
1.18      show ?thesis unfolding prime_elem_def dvd_field_poly
1.19        comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
1.20  qed
1.21 @@ -1314,7 +1314,7 @@
1.22    moreover from assms have "prod_mset B = [:content p:]"
1.23      by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
1.24    moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
1.25 -    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
1.26 +    by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
1.27    ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
1.28  qed
1.29
```