src/Doc/Isar_Ref/Inner_Syntax.thy

     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
     @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
-    @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\<comment> \<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
 
   The token categories @{syntax (inner) num_token}, @{syntax (inner)
   float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},

 
   The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
   (inner) float_const}, provide robust access to the respective tokens: the
   syntax tree holds a syntactic constant instead of a free variable.
 
-  A @{syntax (inner) comment_cartouche} resembles the outer syntax notation
-  for marginal @{syntax_ref comment} (\secref{sec:comments}), but is
-  syntactically more restrictive: only the symbol-form with \<^verbatim>\<open>\<comment>\<close> and text
-  cartouche is supported.
+  Formal document comments (\secref{sec:comments}) may be also used within the
+  inner syntax.
 \<close>
 
 
 subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>