doc-src/Ref/defining.tex

 this is a logical type (namely one of class {\tt logic} excluding {\tt
 prop}).  Otherwise it is $ty$ (note that only the outermost type constructor
 is taken into account).  Finally, the nonterminal of a type variable is {\tt
 any}.
 
-\begin{warn} 
+\begin{warn}
   Theories must sometimes declare types for purely syntactic purposes ---
   merely playing the role of nonterminals. One example is \tydx{type}, the
   built-in type of types.  This is a `type of all types' in the syntactic
   sense only.  Do not declare such types under {\tt arities} as belonging to
   class {\tt logic}\index{*logic class}, for that would make them useless as

 production need not map directly to a logical function (this typically
 requires additional syntactic translations, see also
 Chapter~\ref{chap:syntax}).
 
 
-\medskip 
-As a special case of the general mixfix declaration, the form 
+\medskip
+As a special case of the general mixfix declaration, the form
 \begin{center}
-  {\tt $c$ ::\ "$\sigma$" ("$template$")} 
+  {\tt $c$ ::\ "$\sigma$" ("$template$")}
 \end{center}
 specifies no priorities.  The resulting production puts no priority
 constraints on any of its arguments and has maximal priority itself.
 Omitting priorities in this manner is prone to syntactic ambiguities unless
 the production's right-hand side is fully bracketed, as in \verb|"if _ then _

 \begin{description}
 \item[~$d$~] is a delimiter, namely a non-empty sequence of characters
   other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
   Even these characters may appear if escaped; this means preceding it with
   a~{\tt '} (single quote).  Thus you have to write {\tt ''} if you really
-  want a single quote.  Delimiters may never contain spaces.
+  want a single quote.  Furthermore, a~{\tt '} followed by a space separates
+  delimiters without extra white space being added for printing.
 
 \item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
   or name token.
 
 \item[~$s$~] is a non-empty sequence of spaces for printing.  This and the