changeset 56927 | 4044a7d1720f |
parent 56923 | c062543d380e |
child 56939 | c2ddbf327bbd |
--- a/NEWS Fri May 09 08:13:36 2014 +0200 +++ b/NEWS Fri May 09 08:13:37 2014 +0200 @@ -204,8 +204,11 @@ *** HOL *** +* Command and antiquotation ''value'' are hardcoded against nbe and +ML now. Minor INCOMPATIBILITY. + * Separate command ''approximate'' for approximative computation -in Decision_Procs/Approximation. Minor INCOMPATBILITY. +in Decision_Procs/Approximation. Minor INCOMPATIBILITY. * Adjustion of INF and SUP operations: * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.