--- 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)"
--- a/src/HOL/Multivariate_Analysis/Vec1.thy Mon Apr 26 15:51:10 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy Mon Apr 26 16:28:58 2010 -0700
@@ -394,6 +394,11 @@
hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
- unfolding vec1_dest_vec1_simps by auto qed
+ unfolding vec1_dest_vec1_simps by auto qed
+
+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
end