diff -r f4c079225845 -r c12b25b7f015 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 09:58:11 2009 -0700
@@ -506,8 +506,8 @@
 definition dist_vector_def:
   "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
-definition open_vector_def:
-  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::'a ^ 'b. dist y x < e \<longrightarrow> y \<in> S)"
+definition topo_vector_def:
+  "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
 
 instance proof
   fix x y :: "'a ^ 'b"
@@ -522,9 +522,8 @@
     apply (simp add: setL2_mono dist_triangle2)
     done
 next
-  fix S :: "('a ^ 'b) set"
-  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
-    by (rule open_vector_def)
+  show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+    by (rule topo_vector_def)
 qed
 
 end