NEWS
changeset 50525 46be26e02456
parent 50524 bd145273e7c6
child 50526 899c9c4e4a4c
equal deleted inserted replaced
50524:bd145273e7c6 50525:46be26e02456
   199       less_eq_list.drop ~> less_eq_list_drop
   199       less_eq_list.drop ~> less_eq_list_drop
   200       less_eq_list.induct ~> less_eq_list_induct
   200       less_eq_list.induct ~> less_eq_list_induct
   201       not_le_list_length ~> Sublist.not_sublisteq_length
   201       not_le_list_length ~> Sublist.not_sublisteq_length
   202 
   202 
   203     INCOMPATIBILITY.
   203     INCOMPATIBILITY.
       
   204 
       
   205 * Further generalized the definition of limits:
       
   206 
       
   207   - Introduced the predicate filterlim (LIM x F. f x :> G) which expresses that
       
   208     when the input values x converge to F then the output f x converges to G.
       
   209 
       
   210   - Added filters for convergence to positive (at_top) and negative infinity (at_bot).
       
   211     Moved infinity in the norm (at_infinity) from Multivariate_Analysis to Complex_Main.
       
   212 
       
   213   - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
       
   214     INCOMPATIBILITY
   204 
   215 
   205 * HOL/Rings: renamed lemmas
   216 * HOL/Rings: renamed lemmas
   206 
   217 
   207 left_distrib ~> distrib_right
   218 left_distrib ~> distrib_right
   208 right_distrib ~> distrib_left
   219 right_distrib ~> distrib_left