* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
