# HG changeset patch # User paulson # Date 1528142590 -3600 # Node ID f254e383bfe9bb11eb310e693d3a0219729a52af # Parent 8e9da2d09dc6d4f25b22e7188441f44f50426f6f NEWS: infinite products diff -r 8e9da2d09dc6 -r f254e383bfe9 NEWS --- a/NEWS Mon Jun 04 21:00:21 2018 +0100 +++ b/NEWS Mon Jun 04 21:03:10 2018 +0100 @@ -239,14 +239,14 @@ * Abstract bit operations as part of Main: push_bit, take_bit, drop_bit. -* New, more general, axiomatization of complete_distrib_lattice. +* New, more general, axiomatization of complete_distrib_lattice. The former axioms: "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" -are replaced by +are replaced by "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \ A . f Y \ Y)})" -The instantiations of sets and functions as complete_distrib_lattice +The instantiations of sets and functions as complete_distrib_lattice are moved to Hilbert_Choice.thy because their proofs need the Hilbert -choice operator. The dual of this property is also proved in +choice operator. The dual of this property is also proved in Hilbert_Choice.thy. * New syntax for the minimum/maximum of a function over a finite set: @@ -295,7 +295,7 @@ * Predicate pairwise_coprime abolished, use "pairwise coprime" instead. INCOMPATIBILITY. -* The relator rel_filter on filters has been strengthened to its +* The relator rel_filter on filters has been strengthened to its canonical categorical definition with better properties. INCOMPATIBILITY. * Generalized linear algebra involving linear, span, dependent, dim @@ -308,7 +308,7 @@ * HOL-Algebra: renamed (^) to [^] -* Session HOL-Analysis: Moebius functions, the Riemann mapping +* Session HOL-Analysis: infinite products, Moebius functions, the Riemann mapping theorem, the Vitali covering theorem, change-of-variables results for integration and measures.