--- 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)
-------------------------------------