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