| changeset 58421 | 37cbbd8eb460 |
| parent 58410 | 6d46ad54a2ab |
| child 58512 | dc4d76dfa8f0 |
| child 58524 | f805b366a497 |
--- a/NEWS Mon Sep 22 17:07:18 2014 +0200 +++ b/NEWS Mon Sep 22 21:28:57 2014 +0200 @@ -25,6 +25,10 @@ of numeral signs, particulary in expressions involving infix syntax like "(- 1) ^ n". +* Old inner token category "xnum" has been discontinued. Potential +INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" +token category instead. + *** HOL ***