summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.