# HG changeset patch
# User wenzelm
# Date 1315774565 -7200
# Node ID 340df9f3491fc48507336344f2a3908fdb883f62
# Parent  e099fc6f59bee7e5d9fd48bce40f7ed4c72139b6# Parent  7ca82df6e951619f5f92b65f10f105107418d5dd
merged

diff -r 7ca82df6e951 -r 340df9f3491f NEWS
--- a/NEWS	Sun Sep 11 22:55:26 2011 +0200
+++ b/NEWS	Sun Sep 11 22:56:05 2011 +0200
@@ -94,6 +94,10 @@
 * Theory Library/Saturated provides type of numbers with saturated
 arithmetic.
 
+* Theory Library/Product_Lattice defines a pointwise ordering for the
+product type 'a * 'b, and provides instance proofs for various order
+and lattice type classes.
+
 * Classes bot and top require underlying partial order rather than
 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
@@ -234,7 +238,7 @@
   the_Fin     ~> the_enat
 
 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
-been renamed accordingly.
+been renamed accordingly. INCOMPATIBILITY.
 
 * Theory Limits: Type "'a net" has been renamed to "'a filter", in
 accordance with standard mathematical terminology. INCOMPATIBILITY.