# HG changeset patch
# User haftmann
# Date 1398929432 -7200
# Node ID ab36ec0c8eb5aadb06f068bb5098d1b0fea31c43
# Parent  f7d0520e7be23ea8f67cb5c50b201a7749de83fd
NEWS

diff -r f7d0520e7be2 -r ab36ec0c8eb5 NEWS
--- a/NEWS	Thu May 01 14:07:27 2014 +0200
+++ b/NEWS	Thu May 01 09:30:32 2014 +0200
@@ -193,20 +193,17 @@
 
 *** HOL ***
 
-* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
-INCOMPATIBILITY.
-
-* Default congruence rules strong_INF_cong and strong_SUP_cong,
-with simplifier implication in premises.  Generalized and replace
-former INT_cong, SUP_cong.  INCOMPATIBILITY.
-
-* Consolidated theorem names containing INFI and SUPR: have INF
-and SUP instead uniformly.  INCOMPATIBILITY.
-
-* More aggressive normalization of expressions involving INF and Inf
-or SUP and Sup.  INCOMPATIBILITY.
-
-* INF_image and SUP_image do not unfold composition.
+* Adjustion of INF and SUP operations:
+  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
+  * Consolidated theorem names containing INFI and SUPR: have INF
+  and SUP instead uniformly.
+  * More aggressive normalization of expressions involving INF and Inf
+  or SUP and Sup.
+  * INF_image and SUP_image do not unfold composition.
+  * Dropped facts INF_comp, SUP_comp.
+  * Default congruence rules strong_INF_cong and strong_SUP_cong,
+  with simplifier implication in premises.  Generalize and replace
+  former INT_cong, SUP_cong
 INCOMPATIBILITY.
 
 * Swapped orientation of facts image_comp and vimage_comp:
@@ -222,8 +219,6 @@
   can be restored like this:  declare/using [[simp_legacy_precond]]
   This configuration option will disappear again in the future.
 
-* Dropped facts INF_comp, SUP_comp.  INCOMPATIBILITY.
-
 * HOL-Word:
   * Abandoned fact collection "word_arith_alts", which is a
   duplicate of "word_arith_wis".
@@ -434,7 +429,7 @@
 For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
 max.cobounded1m max.cobounded2 directly.
 
-For min_ac or max_ac, prefor more general collection ac_simps.
+For min_ac or max_ac, prefer more general collection ac_simps.
 
 INCOMPATBILITY.