diff -r 159c07ceb18c -r def3bbe6f2a5 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 25 13:14:33 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 25 14:20:58 2014 +0100
@@ -1319,8 +1319,4 @@
   unfolding vec_lambda_beta
   by auto
 
-lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" 
-  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
-  using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
-
 end