equal
deleted
inserted
replaced
6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** General *** |
10 *** General *** |
|
11 |
|
12 * New, more general, axiomatization of complete_distrib_lattice. |
|
13 The former axioms: |
|
14 "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" |
|
15 are replaced by |
|
16 "Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})" |
|
17 The instantiations of sets and functions as complete_distrib_lattice |
|
18 are moved to Hilbert_Choice.thy because their proofs need the Hilbert |
|
19 choice operator. The dual of this property is also proved in |
|
20 Hilbert_Choice.thy. |
11 |
21 |
12 * Marginal comments need to be written exclusively in the new-style form |
22 * Marginal comments need to be written exclusively in the new-style form |
13 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
23 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
14 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
24 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
15 update_comments" to update existing theory files. |
25 update_comments" to update existing theory files. |