--- a/NEWS Thu Feb 14 12:24:56 2013 +0100
+++ b/NEWS Thu Feb 14 14:14:55 2013 +0100
@@ -10,6 +10,15 @@
(lin)order_topology. Allows to generalize theorems about limits and
order. Instances are reals and extended reals.
+*** HOL ***
+
+* Consolidation of library theories on product orders:
+
+ Product_Lattice ~> Product_Order -- pointwise order on products
+ Product_ord ~> Product_Lexorder -- lexicographic order on products
+
+INCOMPATIBILITY.
+
New in Isabelle2013 (February 2013)
-----------------------------------