--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 15:51:10 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 16:28:58 2010 -0700
@@ -634,11 +634,6 @@
subsection {* The traditional Rolle theorem in one dimension. *}
-lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
- unfolding vector_le_def by auto
-lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
- unfolding vector_less_def by auto
-
lemma rolle: fixes f::"real\<Rightarrow>real"
assumes "a < b" "f a = f b" "continuous_on {a..b} f"
"\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"