NEWS
changeset 44736 db18f4d0cc7d
parent 44680 05ab37be94ed
child 44743 6b917e5877d2
     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