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