changeset 56923 | c062543d380e |
parent 56901 | 2f73ef9eb272 |
child 56927 | 4044a7d1720f |
--- a/NEWS Fri May 09 08:13:36 2014 +0200 +++ b/NEWS Fri May 09 08:13:36 2014 +0200 @@ -204,6 +204,9 @@ *** HOL *** +* Separate command ''approximate'' for approximative computation +in Decision_Procs/Approximation. Minor INCOMPATBILITY. + * Adjustion of INF and SUP operations: * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. * Consolidated theorem names containing INFI and SUPR: have INF