# HG changeset patch
# User huffman
# Date 1165940142 -3600
# Node ID 367477e8458b69026ac82a45d7ce0ce8a0ca99bf
# Parent  9d2761d09d91a10273aa4e80706de60a96267cf3
additions to HOL-Complex

diff -r 9d2761d09d91 -r 367477e8458b NEWS
--- a/NEWS	Tue Dec 12 16:20:57 2006 +0100
+++ b/NEWS	Tue Dec 12 17:15:42 2006 +0100
@@ -724,6 +724,47 @@
 feature is used only for decision, for compatibility with arith. This
 means a goal is either solved or left unchanged, no simplification.
 
+* Real: New axiomatic classes formalize real normed vector spaces and
+algebras, using new overloaded constants scaleR :: real => 'a => 'a
+and norm :: 'a => real.
+
+* Real: New constant of_real :: real => 'a::real_algebra_1 injects from
+reals into other types. The overloaded constant Reals :: 'a set is now
+defined as range of_real; potential INCOMPATIBILITY.
+
+* Hyperreal: Several constants that previously worked only for the reals
+have been generalized, so they now work over arbitrary vector spaces. Type
+annotations may need to be added in some cases; potential INCOMPATIBILITY.
+
+  Infinitesimal  :: ('a::real_normed_vector) star set"
+  HFinite        :: ('a::real_normed_vector) star set"
+  HInfinite      :: ('a::real_normed_vector) star set"
+  approx         :: ('a::real_normed_vector) star => 'a star => bool
+  monad          :: ('a::real_normed_vector) star => 'a star set
+  galaxy         :: ('a::real_normed_vector) star => 'a star set
+  (NS)LIMSEQ     :: [nat, 'a::real_normed_vector, 'a] => bool
+  (NS)convergent :: (nat => 'a::real_normed_vector) => bool
+  (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
+  (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
+  (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
+  is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
+  deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
+
+* Complex: Some complex-specific constants are now abbreviations for
+overloaded ones: complex_of_real = of_real, cmod = norm, hcmod = hnorm.
+Other constants have been entirely removed in favor of the polymorphic
+versions (INCOMPATIBILITY):
+
+  approx        <-- capprox
+  HFinite       <-- CFinite
+  HInfinite     <-- CInfinite
+  Infinitesimal <-- CInfinitesimal
+  monad         <-- cmonad
+  galaxy        <-- cgalaxy
+  (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
+  is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
+  (ns)deriv     <-- (ns)cderiv
+
 
 *** ML ***