NEWS
changeset 51115 7dbd6832a689
parent 51088 0a55ac5bdd92
child 51137 077456580eca
     1.1 --- a/NEWS	Thu Feb 14 12:24:56 2013 +0100
     1.2 +++ b/NEWS	Thu Feb 14 14:14:55 2013 +0100
     1.3 @@ -10,6 +10,15 @@
     1.4  (lin)order_topology. Allows to generalize theorems about limits and
     1.5  order. Instances are reals and extended reals.
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Consolidation of library theories on product orders:
    1.10 +
    1.11 +    Product_Lattice ~> Product_Order -- pointwise order on products
    1.12 +    Product_ord ~> Product_Lexorder -- lexicographic order on products
    1.13 +
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  
    1.17  New in Isabelle2013 (February 2013)
    1.18  -----------------------------------