--- a/NEWS Wed Nov 11 19:22:18 2015 +0100
+++ b/NEWS Thu Nov 12 11:30:56 2015 +0100
@@ -92,7 +92,8 @@
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
* Antiquotation @{theory_text} prints uninterpreted theory source text
-(outer syntax with command keywords etc.).
+(outer syntax with command keywords etc.). This may be used in the short
+form \<^theory_text>\<open>...\<close>.
* Antiquotations @{command}, @{method}, @{attribute} print checked
entities of the Isar language.
@@ -133,11 +134,11 @@
the lack of the surrounding isabelle markup environment in output.
* Document antiquotations @{emph} and @{bold} output LaTeX source
-recursively, adding appropriate text style markup. These are typically
-used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
+recursively, adding appropriate text style markup. These may be used in
+the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
* Document antiquotation @{footnote} outputs LaTeX source recursively,
-marked as \footnote{}. This is typically used in the short form \<^footnote>\<open>...\<close>.
+marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
*** Isar ***
--- a/etc/symbols Wed Nov 11 19:22:18 2015 +0100
+++ b/etc/symbols Thu Nov 12 11:30:56 2015 +0100
@@ -363,6 +363,7 @@
\<^descr> code: 0x0027a7 group: control font: IsabelleText
\<^footnote> code: 0x00204b group: control font: IsabelleText
\<^verbatim> code: 0x0025a9 group: control font: IsabelleText
+\<^theory_text> code: 0x002b1a group: control font: IsabelleText
\<^emph> code: 0x002217 group: control font: IsabelleText
\<^bold> code: 0x002759 group: control font: IsabelleText
\<^sub> code: 0x0021e9 group: control font: IsabelleText