NEWS
changeset 54264 27501a51d847
parent 54250 7d2544dd3988
child 54295 45a5523d4a63
--- a/NEWS	Tue Nov 05 09:45:02 2013 +0100
+++ b/NEWS	Tue Nov 05 09:45:03 2013 +0100
@@ -15,8 +15,6 @@
     even_zero_(nat|int) ~> even_zero
 INCOMPATIBILITY.
 
-*** HOL ***
-
 * Elimination of fact duplicates:
     equals_zero_I ~> minus_unique
     diff_eq_0_iff_eq ~> right_minus_eq
@@ -52,6 +50,15 @@
 or the brute way with
 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
 
+* SUP and INF generalized to conditionally_complete_lattice
+
+* Theory Lubs moved HOL image to HOL-Library. It is replaced by
+Conditionally_Complete_Lattices.   INCOMPATIBILITY.
+
+* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
+instead of explicitly stating boundedness of sets.
+
+
 New in Isabelle2013-1 (November 2013)
 -------------------------------------