--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 05 21:51:30 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 05 13:59:25 2014 -0800
@@ -6377,7 +6377,6 @@
text{* "Isometry" (up to constant bounds) of injective linear map etc. *}
lemma cauchy_isometric:
- fixes x :: "nat \<Rightarrow> 'a::euclidean_space"
assumes e: "e > 0"
and s: "subspace s"
and f: "bounded_linear f"
@@ -6412,7 +6411,6 @@
qed
lemma complete_isometric_image:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "0 < e"
and s: "subspace s"
and f: "bounded_linear f"