NEWS
changeset 66488 9d83e8fe3de3
parent 66481 d35f7a9f92e2
child 66541 4d9c4cb9e9a5
     1.1 --- a/NEWS	Tue Aug 22 21:36:48 2017 +0200
     1.2 +++ b/NEWS	Wed Aug 23 01:05:39 2017 +0200
     1.3 @@ -215,6 +215,9 @@
     1.4  * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
     1.5  been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
     1.6  
     1.7 +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" 
     1.8 +filter for describing points x such that f(x) is in the filter F.
     1.9 +
    1.10  * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
    1.11  renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
    1.12  space. INCOMPATIBILITY.