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

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