NEWS
changeset 67831 07f5588f2735
parent 67830 4f992daf4707
child 67904 465f43a9f780
     1.1 --- a/NEWS	Mon Mar 12 20:53:29 2018 +0100
     1.2 +++ b/NEWS	Mon Mar 12 21:03:57 2018 +0100
     1.3 @@ -9,16 +9,6 @@
     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
    1.20 @@ -204,6 +194,16 @@
    1.21  
    1.22  *** HOL ***
    1.23  
    1.24 +* New, more general, axiomatization of complete_distrib_lattice. 
    1.25 +The former axioms:
    1.26 +"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
    1.27 +are replaced by 
    1.28 +"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
    1.29 +The instantiations of sets and functions as complete_distrib_lattice 
    1.30 +are moved to Hilbert_Choice.thy because their proofs need the Hilbert
    1.31 +choice operator. The dual of this property is also proved in 
    1.32 +Hilbert_Choice.thy.
    1.33 +
    1.34  * Clarifed theorem names:
    1.35  
    1.36    Min.antimono ~> Min.subset_imp