NEWS
changeset 56807 ab36ec0c8eb5
parent 56787 81dc6fffdf30
child 56815 848d507584db
     1.1 --- a/NEWS	Thu May 01 14:07:27 2014 +0200
     1.2 +++ b/NEWS	Thu May 01 09:30:32 2014 +0200
     1.3 @@ -193,20 +193,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
     1.8 -INCOMPATIBILITY.
     1.9 -
    1.10 -* Default congruence rules strong_INF_cong and strong_SUP_cong,
    1.11 -with simplifier implication in premises.  Generalized and replace
    1.12 -former INT_cong, SUP_cong.  INCOMPATIBILITY.
    1.13 -
    1.14 -* Consolidated theorem names containing INFI and SUPR: have INF
    1.15 -and SUP instead uniformly.  INCOMPATIBILITY.
    1.16 -
    1.17 -* More aggressive normalization of expressions involving INF and Inf
    1.18 -or SUP and Sup.  INCOMPATIBILITY.
    1.19 -
    1.20 -* INF_image and SUP_image do not unfold composition.
    1.21 +* Adjustion of INF and SUP operations:
    1.22 +  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
    1.23 +  * Consolidated theorem names containing INFI and SUPR: have INF
    1.24 +  and SUP instead uniformly.
    1.25 +  * More aggressive normalization of expressions involving INF and Inf
    1.26 +  or SUP and Sup.
    1.27 +  * INF_image and SUP_image do not unfold composition.
    1.28 +  * Dropped facts INF_comp, SUP_comp.
    1.29 +  * Default congruence rules strong_INF_cong and strong_SUP_cong,
    1.30 +  with simplifier implication in premises.  Generalize and replace
    1.31 +  former INT_cong, SUP_cong
    1.32  INCOMPATIBILITY.
    1.33  
    1.34  * Swapped orientation of facts image_comp and vimage_comp:
    1.35 @@ -222,8 +219,6 @@
    1.36    can be restored like this:  declare/using [[simp_legacy_precond]]
    1.37    This configuration option will disappear again in the future.
    1.38  
    1.39 -* Dropped facts INF_comp, SUP_comp.  INCOMPATIBILITY.
    1.40 -
    1.41  * HOL-Word:
    1.42    * Abandoned fact collection "word_arith_alts", which is a
    1.43    duplicate of "word_arith_wis".
    1.44 @@ -434,7 +429,7 @@
    1.45  For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
    1.46  max.cobounded1m max.cobounded2 directly.
    1.47  
    1.48 -For min_ac or max_ac, prefor more general collection ac_simps.
    1.49 +For min_ac or max_ac, prefer more general collection ac_simps.
    1.50  
    1.51  INCOMPATBILITY. 
    1.52