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