# HG changeset patch
# User hoelzl
# Date 1355492761 -3600
# Node ID 46be26e02456342e91f66baba1fd325515b7d69a
# Parent bd145273e7c67cab612c6d04c15e41392d87602f
NEWS
diff -r bd145273e7c6 -r 46be26e02456 NEWS
--- a/NEWS Fri Dec 14 12:40:07 2012 +0100
+++ b/NEWS Fri Dec 14 14:46:01 2012 +0100
@@ -202,6 +202,17 @@
INCOMPATIBILITY.
+* Further generalized the definition of limits:
+
+ - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that
+ when the input values x converge to F then the output f x converges to G.
+
+ - Added filters for convergence to positive (at_top) and negative infinity (at_bot).
+ Moved infinity in the norm (at_infinity) from Multivariate_Analysis to Complex_Main.
+
+ - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
+ INCOMPATIBILITY
+
* HOL/Rings: renamed lemmas
left_distrib ~> distrib_right