--- a/NEWS Tue Nov 10 22:27:48 2015 +0100
+++ b/NEWS Tue Nov 10 23:21:02 2015 +0100
@@ -94,6 +94,9 @@
* Antiquotation @{theory_text} prints uninterpreted theory source text
(outer syntax with command keywords etc.).
+* Antiquotations @{command}, @{method}, @{attribute} print checked
+entities of the Isar language.
+
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
standard LaTeX macros of the same names.