--- a/src/HOL/Complex.thy Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Complex.thy Sun Jun 07 17:59:54 2009 -0700
@@ -281,8 +281,8 @@
definition dist_complex_def:
"dist x y = cmod (x - y)"
-definition topo_complex_def [code del]:
- "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+definition open_complex_def [code del]:
+ "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
lemmas cmod_def = complex_norm_def
@@ -290,7 +290,7 @@
by (simp add: complex_norm_def)
instance proof
- fix r :: real and x y :: complex
+ fix r :: real and x y :: complex and S :: "complex set"
show "0 \<le> norm x"
by (induct x) simp
show "(norm x = 0) = (x = 0)"
@@ -308,8 +308,8 @@
by (rule complex_sgn_def)
show "dist x y = cmod (x - y)"
by (rule dist_complex_def)
- show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
- by (rule topo_complex_def)
+ show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ by (rule open_complex_def)
qed
end