# HG changeset patch
# User huffman
# Date 1244939484 25200
# Node ID 937dea81dde0d3e70cbe26f43f2e7b328a101d36
# Parent  f5ffe064412abcc960bee5ca080df288f8a2dd49
generalize lemma connected_real_lemma

diff -r f5ffe064412a -r 937dea81dde0 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sat Jun 13 13:10:10 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Sat Jun 13 17:31:24 2009 -0700
@@ -889,7 +889,7 @@
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
 lemma connected_real_lemma:
-  fixes f :: "real \<Rightarrow> real ^ 'n::finite"
+  fixes f :: "real \<Rightarrow> 'a::metric_space"
   assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
   and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
   and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"