NEWS
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.