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