# HG changeset patch
# User huffman
# Date 1394056765 28800
# Node ID 30c41a8eca0e121025f00ace57c822d0854ef23a
# Parent  3ef14caf5637843ba00f4d9ece75694166fc3860
generalize lemmas

diff -r 3ef14caf5637 -r 30c41a8eca0e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"