src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 58259 52c35a59bbf5
parent 58249 180f1b3508ed
child 58310 91ea607a34d8
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -930,7 +930,7 @@
     1.4    apply (induct p arbitrary: n0)
     1.5    apply auto
     1.6    apply atomize
     1.7 -  apply (erule_tac x = "Suc nat" in allE)
     1.8 +  apply (rename_tac nat a b, erule_tac x = "Suc nat" in allE)
     1.9    apply auto
    1.10    done
    1.11  
    1.12 @@ -1056,7 +1056,7 @@
    1.13  lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
    1.14    apply (cases p)
    1.15    apply auto
    1.16 -  apply (case_tac "nat")
    1.17 +  apply (rename_tac nat a, case_tac "nat")
    1.18    apply simp_all
    1.19    done
    1.20  
    1.21 @@ -1144,7 +1144,7 @@
    1.22    unfolding polypoly_def
    1.23    apply (cases p)
    1.24    apply auto
    1.25 -  apply (case_tac nat)
    1.26 +  apply (rename_tac nat a, case_tac nat)
    1.27    apply auto
    1.28    done
    1.29  
    1.30 @@ -2009,7 +2009,7 @@
    1.31    unfolding isnonconstant_def
    1.32    apply (cases p)
    1.33    apply simp_all
    1.34 -  apply (case_tac nat)
    1.35 +  apply (rename_tac nat a, case_tac nat)
    1.36    apply auto
    1.37    done
    1.38