author | paulson <lp15@cam.ac.uk> |

Mon Jun 04 21:03:10 2018 +0100 (19 months ago ago) | |

changeset 68373 | f254e383bfe9 |

parent 68372 | 8e9da2d09dc6 |

child 68378 | 1d1e9f9f8641 |

NEWS: infinite products

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