even more precise NEWS
authorhaftmann
Mon, 25 Nov 2013 18:18:58 +0100
changeset 54587 19cd731eb745
parent 54586 ebc8f6bf20c0
child 54588 42b9baf50f8f
child 54591 c822230fd22b
even more precise NEWS
NEWS
--- a/NEWS	Mon Nov 25 16:59:02 2013 +0000
+++ b/NEWS	Mon Nov 25 18:18:58 2013 +0100
@@ -28,7 +28,9 @@
   * Canonical representation for minus one is "- 1".
   * Canonical representation for other negative numbers is "- (numeral _)".
   * When devising rule sets for number calculation, consider the
-    following cases: 0, 1, numeral _, - 1, - numeral _.
+    following canonical cases: 0, 1, numeral _, - 1, - numeral _.
+  * HOLogic.dest_number also recognizes numerals in non-canonical forms
+    like "numeral One", "- numeral One", "- 0" and even "- … - _".
   * Syntax for negative numerals is mere input syntax.
 INCOMPATBILITY.