--- a/NEWS Mon Mar 12 20:52:53 2018 +0100
+++ b/NEWS Mon Mar 12 20:53:29 2018 +0100
@@ -9,6 +9,16 @@
*** General ***
+* New, more general, axiomatization of complete_distrib_lattice.
+The former axioms:
+"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"
+are replaced by
+"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})"
+The instantiations of sets and functions as complete_distrib_lattice
+are moved to Hilbert_Choice.thy because their proofs need the Hilbert
+choice operator. The dual of this property is also proved in
+Hilbert_Choice.thy.
+
* Marginal comments need to be written exclusively in the new-style form
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer
supported. INCOMPATIBILITY, use the command-line tool "isabelle