--- 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