author paulson Mon Jun 04 21:03:10 2018 +0100 (19 months ago ago) changeset 68373 f254e383bfe9 parent 68372 8e9da2d09dc6 child 68378 1d1e9f9f8641
NEWS: infinite products
 NEWS file | annotate | diff | revisions
```     1.1 --- a/NEWS	Mon Jun 04 21:00:21 2018 +0100
1.2 +++ b/NEWS	Mon Jun 04 21:03:10 2018 +0100
1.3 @@ -239,14 +239,14 @@
1.4  * Abstract bit operations as part of Main: push_bit, take_bit,
1.5  drop_bit.
1.6
1.7 -* New, more general, axiomatization of complete_distrib_lattice.
1.8 +* New, more general, axiomatization of complete_distrib_lattice.
1.9  The former axioms:
1.10  "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
1.11 -are replaced by
1.12 +are replaced by
1.13  "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
1.14 -The instantiations of sets and functions as complete_distrib_lattice
1.15 +The instantiations of sets and functions as complete_distrib_lattice
1.16  are moved to Hilbert_Choice.thy because their proofs need the Hilbert
1.17 -choice operator. The dual of this property is also proved in
1.18 +choice operator. The dual of this property is also proved in
1.19  Hilbert_Choice.thy.
1.20
1.21  * New syntax for the minimum/maximum of a function over a finite set:
1.22 @@ -295,7 +295,7 @@
1.23  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
1.24  INCOMPATIBILITY.
1.25
1.26 -* The relator rel_filter on filters has been strengthened to its
1.27 +* The relator rel_filter on filters has been strengthened to its
1.28  canonical categorical definition with better properties. INCOMPATIBILITY.
1.29
1.30  * Generalized linear algebra involving linear, span, dependent, dim
1.31 @@ -308,7 +308,7 @@
1.32
1.33  * HOL-Algebra: renamed (^) to [^]
1.34
1.35 -* Session HOL-Analysis: Moebius functions, the Riemann mapping
1.36 +* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping
1.37  theorem, the Vitali covering theorem, change-of-variables results for
1.38  integration and measures.
1.39
```