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

NEWS

changeset 66643 | f7e38b8583a0 |

parent 66641 | ff2e0115fea4 |

child 66650 | bcea02893d17 |

1.1 --- a/NEWS Fri Sep 08 12:49:40 2017 +0100 1.2 +++ b/NEWS Fri Sep 08 15:27:22 2017 +0100 1.3 @@ -220,7 +220,7 @@ 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 +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" 1.9 filter for describing points x such that f(x) is in the filter F. 1.10 1.11 * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been 1.12 @@ -255,7 +255,7 @@ 1.13 1.14 * Session HOL-Analysis: more material involving arcs, paths, covering 1.15 spaces, innessential maps, retracts, infinite products, simplicial complexes. 1.16 -Baire Category theory. Major results include the Jordan Curve Theorem and the Great Picard 1.17 +Baire Category theorem. Major results include the Jordan Curve Theorem and the Great Picard 1.18 Theorem. 1.19 1.20 * Session HOL-Algebra has been extended by additional lattice theory: