summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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