# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1520884409 -3600
# Node ID 4f992daf47078dedaa2690bbb81a52f97ef0bc57
# Parent  2a6ef5ba482263b730af2fac461f52861e4a3154
Changes to NEWS regarding 2a6ef5ba4822

diff -r 2a6ef5ba4822 -r 4f992daf4707 NEWS
--- 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