src/HOL/Library/Polynomial.thy
changeset 56544 b60d5d119489
parent 56383 8e7052e9fda4
child 57482 60459c3853af
     1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -1109,7 +1109,7 @@
     1.4  lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
     1.5    unfolding pos_poly_def
     1.6    apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
     1.7 -  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
     1.8 +  apply (simp add: degree_mult_eq coeff_mult_degree_sum)
     1.9    apply auto
    1.10    done
    1.11