NEWS
changeset 54864 a064732223ad
parent 54850 980817309b78
child 54881 dff57132cf18
     1.1 --- a/NEWS	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/NEWS	Wed Dec 25 17:39:07 2013 +0100
     1.3 @@ -28,6 +28,61 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Abolished slightly odd global lattice interpretation for min/max.
     1.8 +
     1.9 +Fact consolidations:
    1.10 +    min_max.inf_assoc ~> min.assoc
    1.11 +    min_max.inf_commute ~> min.commute
    1.12 +    min_max.inf_left_commute ~> min.left_commute
    1.13 +    min_max.inf_idem ~> min.idem
    1.14 +    min_max.inf_left_idem ~> min.left_idem
    1.15 +    min_max.inf_right_idem ~> min.right_idem
    1.16 +    min_max.sup_assoc ~> max.assoc
    1.17 +    min_max.sup_commute ~> max.commute
    1.18 +    min_max.sup_left_commute ~> max.left_commute
    1.19 +    min_max.sup_idem ~> max.idem
    1.20 +    min_max.sup_left_idem ~> max.left_idem
    1.21 +    min_max.sup_inf_distrib1 ~> max_min_distrib2
    1.22 +    min_max.sup_inf_distrib2 ~> max_min_distrib1
    1.23 +    min_max.inf_sup_distrib1 ~> min_max_distrib2
    1.24 +    min_max.inf_sup_distrib2 ~> min_max_distrib1
    1.25 +    min_max.distrib ~> min_max_distribs
    1.26 +    min_max.inf_absorb1 ~> min.absorb1
    1.27 +    min_max.inf_absorb2 ~> min.absorb2
    1.28 +    min_max.sup_absorb1 ~> max.absorb1
    1.29 +    min_max.sup_absorb2 ~> max.absorb2
    1.30 +    min_max.le_iff_inf ~> min.absorb_iff1
    1.31 +    min_max.le_iff_sup ~> max.absorb_iff2
    1.32 +    min_max.inf_le1 ~> min.cobounded1
    1.33 +    min_max.inf_le2 ~> min.cobounded2
    1.34 +    le_maxI1, min_max.sup_ge1 ~> max.cobounded1
    1.35 +    le_maxI2, min_max.sup_ge2 ~> max.cobounded2
    1.36 +    min_max.le_infI1 ~> min.coboundedI1
    1.37 +    min_max.le_infI2 ~> min.coboundedI2
    1.38 +    min_max.le_supI1 ~> max.coboundedI1
    1.39 +    min_max.le_supI2 ~> max.coboundedI2
    1.40 +    min_max.less_infI1 ~> min.strict_coboundedI1
    1.41 +    min_max.less_infI2 ~> min.strict_coboundedI2
    1.42 +    min_max.less_supI1 ~> max.strict_coboundedI1
    1.43 +    min_max.less_supI2 ~> max.strict_coboundedI2
    1.44 +    min_max.inf_mono ~> min.mono
    1.45 +    min_max.sup_mono ~> max.mono
    1.46 +    min_max.le_infI, min_max.inf_greatest ~> min.boundedI
    1.47 +    min_max.le_supI, min_max.sup_least ~> max.boundedI
    1.48 +    min_max.le_inf_iff ~> min.bounded_iff
    1.49 +    min_max.le_sup_iff ~> max.bounded_iff
    1.50 +
    1.51 +For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
    1.52 +min.left_commute, min.left_idem, max.commute, max.assoc,
    1.53 +max.left_commute, max.left_idem directly.
    1.54 +
    1.55 +For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
    1.56 +max.cobounded1m max.cobounded2 directly.
    1.57 +
    1.58 +For min_ac or max_ac, prefor more general collection ac_simps.
    1.59 +
    1.60 +INCOMPATBILITY. 
    1.61 +
    1.62  * Word library: bit representations prefer type bool over type bit.
    1.63  INCOMPATIBILITY.
    1.64