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