# HG changeset patch
# User huffman
# Date 1272324538 25200
# Node ID bbe2730e6db6dd9fac8ce810a7a9aa9dcd3e88b5
# Parent  2a74926bd76061025ebfdda0ebdf38738095c8cb
more lemmas to Vec1.thy

diff -r 2a74926bd760 -r bbe2730e6db6 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)"
diff -r 2a74926bd760 -r bbe2730e6db6 src/HOL/Multivariate_Analysis/Vec1.thy
--- 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