src/HOL/Complex/NSCA.thy
changeset 14653 0848ab6fe5fc
parent 14469 c7674b7034f5
child 15013 34264f5e4691
     1.1 --- a/src/HOL/Complex/NSCA.thy	Thu Apr 22 11:02:22 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Apr 22 12:11:17 2004 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 +   CInfinitesimal  :: "hcomplex set"
     1.8 +   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
     1.9 +
    1.10      capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
    1.11        --{*the ``infinitely close'' relation*}
    1.12        "x @c= y == (x - y) \<in> CInfinitesimal"     
    1.13 @@ -17,9 +20,6 @@
    1.14     SComplex  :: "hcomplex set"
    1.15     "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
    1.16  
    1.17 -   CInfinitesimal  :: "hcomplex set"
    1.18 -   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
    1.19 -
    1.20     CFinite :: "hcomplex set"
    1.21     "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
    1.22