diff -r 3d89c38408cd -r de19856feb54 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:45:57 2012 +0100
@@ -2891,6 +2891,10 @@
   by (fast intro: less_trans, fast intro: le_less_trans,
     fast intro: order_trans)
 
+lemma atLeastAtMost_singleton_euclidean[simp]:
+  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
+  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
+
 lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
 
 instance real::ordered_euclidean_space