NEWS
changeset 63936 b87784e19a77
parent 63935 aa1fe1103ab8
child 63946 d05da6b707dd
--- a/NEWS	Thu Sep 22 00:12:17 2016 +0200
+++ b/NEWS	Thu Sep 22 11:25:27 2016 +0200
@@ -37,6 +37,8 @@
 symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
 derivatives.
 
+* \<^raw:...> symbols are no longer supported.
+
 * New symbol \<circle>, e.g. for temporal operator.
 
 * Old 'header' command is no longer supported (legacy since