--- a/src/HOL/MacLaurin.thy Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/MacLaurin.thy Thu Feb 05 11:34:42 2009 +0100
@@ -389,15 +389,6 @@
subsection{*Version for Sine Function*}
-lemma MVT2:
- "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
- ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
-apply (drule MVT)
-apply (blast intro: DERIV_isCont)
-apply (force dest: order_less_imp_le simp add: differentiable_def)
-apply (blast dest: DERIV_unique order_less_imp_le)
-done
-
lemma mod_exhaust_less_4:
"m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
by auto