1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Dec 23 20:45:33 2013 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Dec 24 11:24:14 2013 +0100
     1.3 @@ -327,7 +327,7 @@
     1.4  
     1.5  lemma pCons_induct [case_names 0 pCons, induct type: poly]:
     1.6    assumes zero: "P 0"
     1.7 -  assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
     1.8 +  assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)"
     1.9    shows "P p"
    1.10  proof (induct p rule: measure_induct_rule [where f=degree])
    1.11    case (less p)
    1.12 @@ -345,8 +345,14 @@
    1.13      then show "P q"
    1.14        by (rule less.hyps)
    1.15    qed
    1.16 -  then have "P (pCons a q)"
    1.17 -    by (rule pCons)
    1.18 +  have "P (pCons a q)"
    1.19 +  proof (cases "a \<noteq> 0 \<or> q \<noteq> 0")
    1.20 +    case True
    1.21 +    with `P q` show ?thesis by (auto intro: pCons)
    1.22 +  next
    1.23 +    case False
    1.24 +    with zero show ?thesis by simp
    1.25 +  qed
    1.26    then show ?case
    1.27      using `p = pCons a q` by simp
    1.28  qed
    1.29 @@ -412,7 +418,7 @@
    1.30  
    1.31  lemma Poly_coeffs [simp, code abstype]:
    1.32    "Poly (coeffs p) = p"
    1.33 -  by (induct p) (simp_all add: cCons_def)
    1.34 +  by (induct p) auto
    1.35  
    1.36  lemma coeffs_Poly [simp]:
    1.37    "coeffs (Poly as) = strip_while (HOL.eq 0) as"
    1.38 @@ -778,7 +784,7 @@
    1.39  lemma [code]:
    1.40    fixes p q :: "'a::ab_group_add poly"
    1.41    shows "p - q = p + - q"
    1.42 -  by simp
    1.43 +  by (fact ab_add_uminus_conv_diff)
    1.44  
    1.45  lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
    1.46    apply (induct p arbitrary: q, simp)