src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 54489 03ff4d1e6784
parent 54220 0e6645622f22
child 56000 899ad5a3ad00
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -1256,12 +1256,10 @@
     1.4    apply (case_tac n', simp, simp)
     1.5    apply (case_tac n, simp, simp)
     1.6    apply (case_tac n, case_tac n', simp add: Let_def)
     1.7 -  apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
     1.8 -  apply (auto simp add: polyadd_eq_const_degree)
     1.9 +  apply (auto simp add: polyadd_eq_const_degree)[2]
    1.10    apply (metis head_nz)
    1.11    apply (metis head_nz)
    1.12    apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq)
    1.13 -  apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
    1.14    done
    1.15  
    1.16  lemma polymul_head_polyeq: