changeset 56248 | 67dc9549fa15 |
parent 56245 | 84fc7dfa3cd4 |
child 56265 | 785569927666 |
--- a/NEWS Fri Mar 21 22:54:16 2014 +0100 +++ b/NEWS Sat Mar 22 08:37:43 2014 +0100 @@ -138,6 +138,10 @@ * 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.