src/HOL/Complex.thy
changeset 37767 a2b7a20d6ea3
parent 36825 d9320cdcde73
child 37887 2ae085b07f2f
     1.1 --- a/src/HOL/Complex.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Complex.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4  definition dist_complex_def:
     1.5    "dist x y = cmod (x - y)"
     1.6  
     1.7 -definition open_complex_def [code del]:
     1.8 +definition open_complex_def:
     1.9    "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.10  
    1.11  lemmas cmod_def = complex_norm_def