1.1 --- a/NEWS	Tue Nov 05 09:45:02 2013 +0100
     1.2 +++ b/NEWS	Tue Nov 05 09:45:03 2013 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4      even_zero_(nat|int) ~> even_zero
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -*** HOL ***
     1.8 -
     1.9  * Elimination of fact duplicates:
    1.10      equals_zero_I ~> minus_unique
    1.11      diff_eq_0_iff_eq ~> right_minus_eq
    1.12 @@ -52,6 +50,15 @@
    1.13  or the brute way with
    1.14  "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
    1.15  
    1.16 +* SUP and INF generalized to conditionally_complete_lattice
    1.17 +
    1.18 +* Theory Lubs moved HOL image to HOL-Library. It is replaced by
    1.19 +Conditionally_Complete_Lattices.   INCOMPATIBILITY.
    1.20 +
    1.21 +* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
    1.22 +instead of explicitly stating boundedness of sets.
    1.23 +
    1.24 +
    1.25  New in Isabelle2013-1 (November 2013)
    1.26  -------------------------------------
    1.27