NEWS
changeset 21791 367477e8458b
parent 21735 0c65e072f4be
child 21879 a3efbae45735
     1.1 --- a/NEWS	Tue Dec 12 16:20:57 2006 +0100
     1.2 +++ b/NEWS	Tue Dec 12 17:15:42 2006 +0100
     1.3 @@ -724,6 +724,47 @@
     1.4  feature is used only for decision, for compatibility with arith. This
     1.5  means a goal is either solved or left unchanged, no simplification.
     1.6  
     1.7 +* Real: New axiomatic classes formalize real normed vector spaces and
     1.8 +algebras, using new overloaded constants scaleR :: real => 'a => 'a
     1.9 +and norm :: 'a => real.
    1.10 +
    1.11 +* Real: New constant of_real :: real => 'a::real_algebra_1 injects from
    1.12 +reals into other types. The overloaded constant Reals :: 'a set is now
    1.13 +defined as range of_real; potential INCOMPATIBILITY.
    1.14 +
    1.15 +* Hyperreal: Several constants that previously worked only for the reals
    1.16 +have been generalized, so they now work over arbitrary vector spaces. Type
    1.17 +annotations may need to be added in some cases; potential INCOMPATIBILITY.
    1.18 +
    1.19 +  Infinitesimal  :: ('a::real_normed_vector) star set"
    1.20 +  HFinite        :: ('a::real_normed_vector) star set"
    1.21 +  HInfinite      :: ('a::real_normed_vector) star set"
    1.22 +  approx         :: ('a::real_normed_vector) star => 'a star => bool
    1.23 +  monad          :: ('a::real_normed_vector) star => 'a star set
    1.24 +  galaxy         :: ('a::real_normed_vector) star => 'a star set
    1.25 +  (NS)LIMSEQ     :: [nat, 'a::real_normed_vector, 'a] => bool
    1.26 +  (NS)convergent :: (nat => 'a::real_normed_vector) => bool
    1.27 +  (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
    1.28 +  (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
    1.29 +  (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
    1.30 +  is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
    1.31 +  deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
    1.32 +
    1.33 +* Complex: Some complex-specific constants are now abbreviations for
    1.34 +overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = hnorm.
    1.35 +Other constants have been entirely removed in favor of the polymorphic
    1.36 +versions (INCOMPATIBILITY):
    1.37 +
    1.38 +  approx        <-- capprox
    1.39 +  HFinite       <-- CFinite
    1.40 +  HInfinite     <-- CInfinite
    1.41 +  Infinitesimal <-- CInfinitesimal
    1.42 +  monad         <-- cmonad
    1.43 +  galaxy        <-- cgalaxy
    1.44 +  (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
    1.45 +  is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
    1.46 +  (ns)deriv     <-- (ns)cderiv
    1.47 +
    1.48  
    1.49  *** ML ***
    1.50