# HG changeset patch
# User huffman
# Date 1315774182 25200
# Node ID e099fc6f59bee7e5d9fd48bce40f7ed4c72139b6
# Parent  6ca299d29bdd28b4e0337090845c7ff4561755a6
NEWS for Library/Product_Lattice.thy

diff -r 6ca299d29bdd -r e099fc6f59be NEWS
--- a/NEWS	Sun Sep 11 21:35:35 2011 +0200
+++ b/NEWS	Sun Sep 11 13:49:42 2011 -0700
@@ -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.