--- a/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:38 2017 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:40 2017 +0200
@@ -16,8 +16,8 @@
subsection \<open>Various facts about polynomials\<close>
-lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
- by (induction A) (simp_all add: one_poly_def mult_ac)
+lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
+ by (induct A) (simp_all add: one_poly_def ac_simps)
lemma irreducible_const_poly_iff:
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
@@ -169,13 +169,14 @@
lemma prod_mset_fract_poly:
"prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
- by (induction A) (simp_all add: mult_ac)
+ by (induct A) (simp_all add: one_poly_def ac_simps)
lemma is_unit_fract_poly_iff:
"p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
proof safe
assume A: "p dvd 1"
- with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
+ with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)"
+ by simp
from A show "content p = 1"
by (auto simp: is_unit_poly_iff normalize_1_iff)
next