[isabelle-dev] NEWS: filterlim

Johannes Hölzl hoelzl at in.tum.de
Fri Dec 14 15:56:43 CET 2012

* 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".

More information about the isabelle-dev mailing list