NEWS
authorhoelzl
Fri Dec 14 14:46:01 2012 +0100 (2012-12-14)
changeset 5052546be26e02456
parent 50524 bd145273e7c6
child 50526 899c9c4e4a4c
NEWS
NEWS
     1.1 --- a/NEWS	Fri Dec 14 12:40:07 2012 +0100
     1.2 +++ b/NEWS	Fri Dec 14 14:46:01 2012 +0100
     1.3 @@ -202,6 +202,17 @@
     1.4  
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* Further generalized the definition of limits:
     1.8 +
     1.9 +  - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that
    1.10 +    when the input values x converge to F then the output f x converges to G.
    1.11 +
    1.12 +  - Added filters for convergence to positive (at_top) and negative infinity (at_bot).
    1.13 +    Moved infinity in the norm (at_infinity) from Multivariate_Analysis to Complex_Main.
    1.14 +
    1.15 +  - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
    1.16 +    INCOMPATIBILITY
    1.17 +
    1.18  * HOL/Rings: renamed lemmas
    1.19  
    1.20  left_distrib ~> distrib_right