src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 60580 7e741e22d7fc
parent 60537 5398aa5a4df9
child 60698 29e8bdc41f90
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -908,13 +908,13 @@
     1.4  subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
     1.5  
     1.6  lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
     1.7 -proof (induct p arbitrary: n rule: poly.induct, auto)
     1.8 -  case (goal1 c n p n')
     1.9 +proof (induct p arbitrary: n rule: poly.induct, auto, goals)
    1.10 +  case prems: (1 c n p n')
    1.11    then have "n = Suc (n - 1)"
    1.12      by simp
    1.13    then have "isnpolyh p (Suc (n - 1))"
    1.14      using \<open>isnpolyh p n\<close> by simp
    1.15 -  with goal1(2) show ?case
    1.16 +  with prems(2) show ?case
    1.17      by simp
    1.18  qed
    1.19