# HG changeset patch
# User haftmann
# Date 1491392860 -7200
# Node ID 6f9c6ae27984a787f4e64d7358272d625128d551
# Parent  a8d868477bc01deed32c46ff5c14562e3280b717
tuned

diff -r a8d868477bc0 -r 6f9c6ae27984 src/HOL/Library/Polynomial_Factorial.thy
--- 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