--- a/NEWS Wed Sep 21 22:44:24 2016 +0200
+++ b/NEWS Thu Sep 22 00:12:17 2016 +0200
@@ -33,6 +33,10 @@
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
this allows special forms of document output.
+* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
+symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
+derivatives.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since