changeset 35130 | 0991c84e8dcf |
parent 35129 | ed24ba6f69aa |
child 35260 | 41e82c1b5586 |
child 35264 | f44ef0e2d178 |
--- a/NEWS Mon Feb 15 17:17:51 2010 +0100 +++ b/NEWS Mon Feb 15 18:03:42 2010 +0100 @@ -10,7 +10,9 @@ the user space functionality any longer. * Discontinued unnamed infix syntax (legacy feature for many years) -- -need to specify constant name and syntax separately. +need to specify constant name and syntax separately. Internal ML +datatype constructors have been renamed from InfixName to Infix etc. +Minor INCOMPATIBILITY. *** HOL ***