1.1 --- a/src/HOL/Complex.thy	Sun Jun 07 15:18:52 2009 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun Jun 07 17:59:54 2009 -0700
     1.3 @@ -281,8 +281,8 @@
     1.4  definition dist_complex_def:
     1.5    "dist x y = cmod (x - y)"
     1.6  
     1.7 -definition topo_complex_def [code del]:
     1.8 -  "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
     1.9 +definition open_complex_def [code del]:
    1.10 +  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.11  
    1.12  lemmas cmod_def = complex_norm_def
    1.13  
    1.14 @@ -290,7 +290,7 @@
    1.15    by (simp add: complex_norm_def)
    1.16  
    1.17  instance proof
    1.18 -  fix r :: real and x y :: complex
    1.19 +  fix r :: real and x y :: complex and S :: "complex set"
    1.20    show "0 \<le> norm x"
    1.21      by (induct x) simp
    1.22    show "(norm x = 0) = (x = 0)"
    1.23 @@ -308,8 +308,8 @@
    1.24      by (rule complex_sgn_def)
    1.25    show "dist x y = cmod (x - y)"
    1.26      by (rule dist_complex_def)
    1.27 -  show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.28 -    by (rule topo_complex_def)
    1.29 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.30 +    by (rule open_complex_def)
    1.31  qed
    1.32  
    1.33  end