src/Doc/Isar_Ref/Inner_Syntax.thy

 
   \<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
   used internally in Isabelle/Pure.
 
   \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols
-  instead of ASCII art.\footnote{This traditional mode name stems from
-  the ``X-Symbol'' package for classic Proof~General with XEmacs.}
+  instead of ASCII art.\<^footnote>\<open>This traditional mode name stems from
+  the ``X-Symbol'' package for classic Proof~General with XEmacs.\<close>
 
   \<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
   document preparation of Isabelle theory sources; allows to provide
   alternative output notation.
 \<close>

 
   Altogether this determines a production for a context-free priority
   grammar, where for each argument \<open>i\<close> the syntactic category
   is determined by \<open>\<tau>\<^sub>i\<close> (with priority \<open>p\<^sub>i\<close>), and the
   result category is determined from \<open>\<tau>\<close> (with priority \<open>p\<close>).  Priority specifications are optional, with default 0 for
-  arguments and 1000 for the result.\footnote{Omitting priorities is
+  arguments and 1000 for the result.\<^footnote>\<open>Omitting priorities is
   prone to syntactic ambiguities unless the delimiter tokens determine
-  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.}
+  fully bracketed notation, as in \<open>if _ then _ else _ fi\<close>.\<close>
 
   Since \<open>\<tau>\<close> may be again a function type, the constant
   type scheme may have more argument positions than the mixfix
   pattern.  Printing a nested application \<open>c t\<^sub>1 \<dots> t\<^sub>m\<close> for
   \<open>m > n\<close> works by attaching concrete notation only to the

 
   AST rewrite rules \<open>(lhs, rhs)\<close> need to obey the following
   side-conditions:
 
     \<^item> Rules must be left linear: \<open>lhs\<close> must not contain
-    repeated variables.\footnote{The deeper reason for this is that AST
+    repeated variables.\<^footnote>\<open>The deeper reason for this is that AST
     equality is not well-defined: different occurrences of the ``same''
     AST could be decorated differently by accidental type-constraints or
-    source position information, for example.}
+    source position information, for example.\<close>
 
     \<^item> Every variable in \<open>rhs\<close> must also occur in \<open>lhs\<close>.
 
   \<^descr> @{command "no_translations"}~\<open>rules\<close> removes syntactic
   translation rules, which are interpreted in the same manner as for