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
```