1.1 --- a/NEWS Sun Jul 17 08:45:06 2011 +0200
1.2 +++ b/NEWS Sun Jul 17 15:15:58 2011 +0200
1.3 @@ -63,6 +63,11 @@
1.4 * Classes bot and top require underlying partial order rather than preorder:
1.5 uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
1.6
1.7 +* Class 'complete_lattice': generalized a couple of lemmas from sets;
1.8 +generalized theorems INF_cong and SUP_cong. More consistent names: TBD.
1.9 +
1.10 +INCOMPATIBILITY.
1.11 +
1.12 * Archimedian_Field.thy:
1.13 floor now is defined as parameter of a separate type class floor_ceiling.
1.14