src/HOL/MacLaurin.thy
changeset 29803 c56a5571f60a
parent 29187 7b09385234f9
child 29811 026b0f9f579f
     1.1 --- a/src/HOL/MacLaurin.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Thu Feb 05 11:34:42 2009 +0100
     1.3 @@ -389,15 +389,6 @@
     1.4  
     1.5  subsection{*Version for Sine Function*}
     1.6  
     1.7 -lemma MVT2:
     1.8 -     "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
     1.9 -      ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
    1.10 -apply (drule MVT)
    1.11 -apply (blast intro: DERIV_isCont)
    1.12 -apply (force dest: order_less_imp_le simp add: differentiable_def)
    1.13 -apply (blast dest: DERIV_unique order_less_imp_le)
    1.14 -done
    1.15 -
    1.16  lemma mod_exhaust_less_4:
    1.17    "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
    1.18  by auto