src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 61166 5976fe402824
parent 60698 29e8bdc41f90
child 61586 5197a2ecb658
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 16:50:12 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 20:20:16 2015 +0200
     1.3 @@ -891,7 +891,7 @@
     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, goals)
     1.8 +proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases)
     1.9    case prems: (1 c n p n')
    1.10    then have "n = Suc (n - 1)"
    1.11      by simp