--- a/NEWS Wed Oct 21 18:00:12 2015 +0200
+++ b/NEWS Wed Oct 21 19:23:14 2015 +0200
@@ -62,7 +62,9 @@
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
-\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
+\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The
+standard Isabelle fonts provide glyphs to render important control
+symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
--- a/etc/symbols Wed Oct 21 18:00:12 2015 +0200
+++ b/etc/symbols Wed Oct 21 19:23:14 2015 +0200
@@ -359,6 +359,7 @@
\<^item> code: 0x0025aa group: control font: IsabelleText
\<^enum> code: 0x0025b8 group: control font: IsabelleText
\<^descr> code: 0x0027a7 group: control font: IsabelleText
+\<^verbatim> code: 0x0025a9 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