--- a/NEWS Mon Dec 28 19:23:15 2015 +0100
+++ b/NEWS Mon Dec 28 21:47:32 2015 +0100
@@ -375,6 +375,11 @@
*** HOL ***
+* Former "xsymbols" syntax with Isabelle symbols is used by default,
+without any special print mode. Important ASCII replacement syntax
+remains available under print mode "ASCII", but less important syntax
+has been removed (see below).
+
* Combinator to represent case distinction on products is named "case_prod",
uniformly, discontinuing any input aliasses. Very popular theorem aliasses
have been retained.