| changeset 58410 | 6d46ad54a2ab |
| parent 58373 | 4bdd00a76e54 |
| child 58421 | 37cbbd8eb460 |
--- a/NEWS Sun Sep 21 16:56:06 2014 +0200 +++ b/NEWS Sun Sep 21 16:56:11 2014 +0200 @@ -20,6 +20,11 @@ * Command "class_deps" takes optional sort arguments constraining the search space. +* Lexical separation of signed and unsigend numerals: categories "num" +and "float" are unsigend. INCOMPATIBILITY: subtle change in precedence +of numeral signs, particulary in expressions involving infix syntax like +"(- 1) ^ n". + *** HOL ***