--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 21 20:33:44 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 21 22:43:06 2016 +0200
@@ -329,20 +329,21 @@
printing, notably spaces, blocks, and breaks. The general template format is
a sequence over any of the following entities.
- \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
- the following special characters:
-
- \<^medskip>
- \begin{tabular}{ll}
- \<^verbatim>\<open>'\<close> & single quote \\
- \<^verbatim>\<open>_\<close> & underscore \\
- \<open>\<index>\<close> & index symbol \\
- \<^verbatim>\<open>(\<close> & open parenthesis \\
- \<^verbatim>\<open>)\<close> & close parenthesis \\
- \<^verbatim>\<open>/\<close> & slash \\
- \<open>\<open> \<close>\<close> & cartouche delimiters \\
- \end{tabular}
- \<^medskip>
+ \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence delimiter items of the
+ following form:
+ \<^enum> a control symbol followed by a cartouche
+ \<^enum> a single symbol, excluding the following special characters:
+ \<^medskip>
+ \begin{tabular}{ll}
+ \<^verbatim>\<open>'\<close> & single quote \\
+ \<^verbatim>\<open>_\<close> & underscore \\
+ \<open>\<index>\<close> & index symbol \\
+ \<^verbatim>\<open>(\<close> & open parenthesis \\
+ \<^verbatim>\<open>)\<close> & close parenthesis \\
+ \<^verbatim>\<open>/\<close> & slash \\
+ \<open>\<open> \<close>\<close> & cartouche delimiters \\
+ \end{tabular}
+ \<^medskip>
\<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
literal version of the following character, unless that is a blank.