src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 41842 d8f76db6a207
parent 41816 7a55699805dc
child 45129 1fce03e3e8ad
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Feb 25 08:46:52 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Feb 25 14:25:41 2011 +0100
     1.3 @@ -210,11 +210,6 @@
     1.4    "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
     1.5  | "poly_deriv p = 0\<^sub>p"
     1.6  
     1.7 -  (* Verification *)
     1.8 -lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
     1.9 -using Nat.gr0_conv_Suc
    1.10 -by clarsimp
    1.11 -
    1.12  subsection{* Semantics of the polynomial representation *}
    1.13  
    1.14  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where