NEWS
changeset 67830 4f992daf4707
parent 67764 0f8cb5568b63
child 67831 07f5588f2735
     1.1 --- a/NEWS	Mon Mar 12 20:52:53 2018 +0100
     1.2 +++ b/NEWS	Mon Mar 12 20:53:29 2018 +0100
     1.3 @@ -9,6 +9,16 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* New, more general, axiomatization of complete_distrib_lattice. 
     1.8 +The former axioms:
     1.9 +"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
    1.10 +are replaced by 
    1.11 +"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
    1.12 +The instantiations of sets and functions as complete_distrib_lattice 
    1.13 +are moved to Hilbert_Choice.thy because their proofs need the Hilbert
    1.14 +choice operator. The dual of this property is also proved in 
    1.15 +Hilbert_Choice.thy.
    1.16 +
    1.17  * Marginal comments need to be written exclusively in the new-style form
    1.18  "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
    1.19  supported. INCOMPATIBILITY, use the command-line tool "isabelle