# HG changeset patch
# User hoelzl
# Date 1383641103 -3600
# Node ID 27501a51d847012dde0c2a73145c9668d08ab716
# Parent  c4159fe6fa46dda3bf3e09960e04d476f7f1c0f9
NEWS

diff -r c4159fe6fa46 -r 27501a51d847 NEWS
--- 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)
 -------------------------------------