src/HOL/Complex.thy
changeset 31492 5400beeddb55
parent 31419 74fc28c5d68c
child 36349 39be26d1bc28
--- 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