1.1 --- a/NEWS	Sun Jul 17 20:46:51 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 17 20:57:56 2011 +0200
     1.3 @@ -64,8 +64,13 @@
     1.4  uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
     1.5  
     1.6  * Class 'complete_lattice': generalized a couple of lemmas from sets;
     1.7 -generalized theorems INF_cong and SUP_cong.  More consistent names: TBD.
     1.8 -
     1.9 +generalized theorems INF_cong and SUP_cong.  More consistent and less
    1.10 +misunderstandable names:
    1.11 +  INFI_def ~> INF_def
    1.12 +  SUPR_def ~> SUP_def
    1.13 +  le_SUPI ~> le_SUP_I
    1.14 +  le_SUPI2 ~> le_SUP_I2
    1.15 +  le_INFI ~> le_INF_I
    1.16  INCOMPATIBILITY.
    1.17  
    1.18  * Archimedian_Field.thy: