NEWS: infinite products
authorpaulson <lp15@cam.ac.uk>
Mon Jun 04 21:03:10 2018 +0100 (13 months ago)
changeset 68373f254e383bfe9
parent 68372 8e9da2d09dc6
child 68377 1d1e9f9f8641
NEWS: infinite products
NEWS
     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