doc-src/IsarRef/Thy/document/Inner_Syntax.tex
author wenzelm
Fri Feb 17 15:42:26 2012 +0100 (2012-02-17)
changeset 46512 4f9f61f9b535
parent 46506 c7faa011bfa7
child 46525 af3df09590f9
permissions -rw-r--r--
simplified configuration options for syntax ambiguity;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Inner{\isaliteral{5F}{\isacharunderscore}}Syntax}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Inner{\isaliteral{5F}{\isacharunderscore}}Syntax\isanewline
    12 \isakeyword{imports}\ Base\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 The inner syntax of Isabelle provides concrete notation for
    27   the main entities of the logical framework, notably \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms with types and type classes.  Applications may either
    28   extend existing syntactic categories by additional notation, or
    29   define new sub-languages that are linked to the standard term
    30   language via some explicit markers.  For example \verb|FOO|~\isa{{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}} could embed the syntax corresponding for some
    31   user-defined nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}foo{\isaliteral{22}{\isachardoublequote}}} --- within the bounds of the
    32   given lexical syntax of Isabelle/Pure.
    33 
    34   The most basic way to specify concrete syntax for logical entities
    35   works via mixfix annotations (\secref{sec:mixfix}), which may be
    36   usually given as part of the original declaration or via explicit
    37   notation commands later on (\secref{sec:notation}).  This already
    38   covers many needs of concrete syntax without having to understand
    39   the full complexity of inner syntax layers.
    40 
    41   Further details of the syntax engine involves the classical
    42   distinction of lexical language versus context-free grammar (see
    43   \secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
    44   translations} --- either as rewrite systems on first-order ASTs
    45   (\secref{sec:syn-trans}) or ML functions on ASTs or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-terms that represent parse trees (\secref{sec:tr-funs}).%
    46 \end{isamarkuptext}%
    47 \isamarkuptrue%
    48 %
    49 \isamarkupsection{Printing logical entities%
    50 }
    51 \isamarkuptrue%
    52 %
    53 \isamarkupsubsection{Diagnostic commands \label{sec:print-diag}%
    54 }
    55 \isamarkuptrue%
    56 %
    57 \begin{isamarkuptext}%
    58 \begin{matharray}{rcl}
    59     \indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    60     \indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    61     \indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    62     \indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    63     \indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    64     \indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    65     \indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    66   \end{matharray}
    67 
    68   These diagnostic commands assist interactive development by printing
    69   internal logical entities in a human-readable fashion.
    70 
    71   \begin{railoutput}
    72 \rail@begin{2}{}
    73 \rail@term{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}[]
    74 \rail@bar
    75 \rail@nextbar{1}
    76 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
    77 \rail@endbar
    78 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
    79 \rail@end
    80 \rail@begin{2}{}
    81 \rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
    82 \rail@bar
    83 \rail@nextbar{1}
    84 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
    85 \rail@endbar
    86 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
    87 \rail@end
    88 \rail@begin{2}{}
    89 \rail@term{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}[]
    90 \rail@bar
    91 \rail@nextbar{1}
    92 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
    93 \rail@endbar
    94 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
    95 \rail@end
    96 \rail@begin{2}{}
    97 \rail@term{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}[]
    98 \rail@bar
    99 \rail@nextbar{1}
   100 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
   101 \rail@endbar
   102 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   103 \rail@end
   104 \rail@begin{2}{}
   105 \rail@bar
   106 \rail@term{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}[]
   107 \rail@nextbar{1}
   108 \rail@term{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isaliteral{5F}{\isacharunderscore}}prf}}}}}[]
   109 \rail@endbar
   110 \rail@bar
   111 \rail@nextbar{1}
   112 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
   113 \rail@endbar
   114 \rail@bar
   115 \rail@nextbar{1}
   116 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   117 \rail@endbar
   118 \rail@end
   119 \rail@begin{2}{}
   120 \rail@term{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}[]
   121 \rail@bar
   122 \rail@nextbar{1}
   123 \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
   124 \rail@endbar
   125 \rail@bar
   126 \rail@nextbar{1}
   127 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   128 \rail@endbar
   129 \rail@end
   130 \rail@begin{2}{\indexdef{}{syntax}{modes}\hypertarget{syntax.modes}{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}}
   131 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
   132 \rail@plus
   133 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
   134 \rail@nextplus{1}
   135 \rail@endplus
   136 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   137 \rail@end
   138 \end{railoutput}
   139 
   140 
   141   \begin{description}
   142 
   143   \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints types of the
   144   meta-logic according to the current theory or proof context.
   145 
   146   \item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}
   147   read, type-check and print terms or propositions according to the
   148   current theory or proof context; the inferred type of \isa{t} is
   149   output as well.  Note that these commands are also useful in
   150   inspecting the current environment of term abbreviations.
   151 
   152   \item \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} retrieves
   153   theorems from the current theory or proof context.  Note that any
   154   attributes included in the theorem specifications are applied to a
   155   temporary context derived from the current theory or proof; the
   156   result is discarded, i.e.\ attributes involved in \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} do not have any permanent effect.
   157 
   158   \item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the
   159   current proof state (if present), or of the given theorems. Note
   160   that this requires proof terms to be switched on for the current
   161   object logic (see the ``Proof terms'' section of the Isabelle
   162   reference manual for information on how to do this).
   163 
   164   \item \hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isaliteral{5F}{\isacharunderscore}}prf}}}} is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
   165   the full proof term, i.e.\ also displays information omitted in the
   166   compact proof term, which is denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' placeholders
   167   there.
   168 
   169   \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}goals{\isaliteral{22}{\isachardoublequote}}} prints the current proof state
   170   (if present), including current facts and goals.  The optional limit
   171   arguments affect the number of goals to be displayed, which is
   172   initially 10.  Omitting limit value leaves the current setting
   173   unchanged.
   174 
   175   \end{description}
   176 
   177   All of the diagnostic commands above admit a list of \isa{modes}
   178   to be specified, which is appended to the current print mode; see
   179   also \secref{sec:print-modes}.  Thus the output behavior may be
   180   modified according particular print mode features.  For example,
   181   \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}latex\ xsymbols{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} would print the current
   182   proof state with mathematical symbols and special characters
   183   represented in {\LaTeX} source, according to the Isabelle style
   184   \cite{isabelle-sys}.
   185 
   186   Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
   187   systematic way to include formal items into the printed text
   188   document.%
   189 \end{isamarkuptext}%
   190 \isamarkuptrue%
   191 %
   192 \isamarkupsubsection{Details of printed content%
   193 }
   194 \isamarkuptrue%
   195 %
   196 \begin{isamarkuptext}%
   197 \begin{tabular}{rcll}
   198     \indexdef{}{attribute}{show\_types}\hypertarget{attribute.show-types}{\hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}} & : & \isa{attribute} & default \isa{false} \\
   199     \indexdef{}{attribute}{show\_sorts}\hypertarget{attribute.show-sorts}{\hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}} & : & \isa{attribute} & default \isa{false} \\
   200     \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
   201     \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
   202     \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
   203     \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\
   204     \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\
   205     \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\
   206     \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
   207     \indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
   208     \indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\
   209     \indexdef{}{attribute}{show\_hyps}\hypertarget{attribute.show-hyps}{\hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}} & : & \isa{attribute} & default \isa{false} \\
   210     \indexdef{}{attribute}{show\_tags}\hypertarget{attribute.show-tags}{\hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}}} & : & \isa{attribute} & default \isa{false} \\
   211     \indexdef{}{attribute}{show\_question\_marks}\hypertarget{attribute.show-question-marks}{\hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}}} & : & \isa{attribute} & default \isa{true} \\
   212   \end{tabular}
   213   \medskip
   214 
   215   These configuration options control the detail of information that
   216   is displayed for types, terms, theorems, goals etc.  See also
   217   \secref{sec:config}.
   218 
   219   \begin{description}
   220 
   221   \item \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} and \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} control
   222   printing of type constraints for term variables, and sort
   223   constraints for type variables.  By default, neither of these are
   224   shown in output.  If \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} is enabled, types are
   225   always shown as well.
   226 
   227   Note that displaying types and sorts may explain why a polymorphic
   228   inference rule fails to resolve with some goal, or why a rewrite
   229   rule does not apply as expected.
   230 
   231   \item \hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}} controls printing of types of
   232   constants when displaying a goal state.
   233 
   234   Note that the output can be enormous, because polymorphic constants
   235   often occur at several different type instances.
   236 
   237   \item \hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}} controls folding of constant
   238   abbreviations.
   239 
   240   \item \hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}} controls bracketing in pretty
   241   printed output.  If enabled, all sub-expressions of the pretty
   242   printing tree will be parenthesized, even if this produces malformed
   243   term syntax!  This crude way of showing the internal structure of
   244   pretty printed entities may occasionally help to diagnose problems
   245   with operator priorities, for example.
   246 
   247   \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and
   248   \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully
   249   qualified internal names in external form.  See also
   250   \secref{sec:antiq} for the document antiquotation options of the
   251   same names.
   252 
   253   \item \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted
   254   printing of terms.
   255 
   256   The \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contraction law asserts \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ f{\isaliteral{22}{\isachardoublequote}}},
   257   provided \isa{x} is not free in \isa{f}.  It asserts
   258   \emph{extensionality} of functions: \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g\ x{\isaliteral{22}{\isachardoublequote}}} for all \isa{x}.  Higher-order unification frequently puts
   259   terms into a fully \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded form.  For example, if \isa{F} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} then its expanded form is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
   260 
   261   Enabling \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} makes Isabelle perform \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contractions before printing, so that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
   262   appears simply as \isa{F}.
   263 
   264   Note that the distinction between a term and its \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded
   265   form occasionally matters.  While higher-order resolution and
   266   rewriting operate modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-conversion, some other tools
   267   might look at terms more discretely.
   268 
   269   \item \hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}} controls the maximum number of
   270   subgoals to be shown in goal output.
   271 
   272   \item \hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}} controls whether the main result
   273   to be proven should be displayed.  This information might be
   274   relevant for schematic goals, to inspect the current claim that has
   275   been synthesized so far.
   276 
   277   \item \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}} controls printing of implicit
   278   hypotheses of local facts.  Normally, only those hypotheses are
   279   displayed that are \emph{not} covered by the assumptions of the
   280   current context: this situation indicates a fault in some tool being
   281   used.
   282 
   283   By enabling \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}, output of \emph{all} hypotheses
   284   can be enforced, which is occasionally useful for diagnostic
   285   purposes.
   286 
   287   \item \hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}} controls printing of extra annotations
   288   within theorems, such as internal position information, or the case
   289   names being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}.
   290 
   291   Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}
   292   attributes provide low-level access to the collection of tags
   293   associated with a theorem.
   294 
   295   \item \hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}} controls printing of question
   296   marks for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}.  Only the leading
   297   question mark is affected, the remaining text is unchanged
   298   (including proper markup for schematic variables that might be
   299   relevant for user interfaces).
   300 
   301   \end{description}%
   302 \end{isamarkuptext}%
   303 \isamarkuptrue%
   304 %
   305 \isamarkupsubsection{Alternative print modes \label{sec:print-modes}%
   306 }
   307 \isamarkuptrue%
   308 %
   309 \begin{isamarkuptext}%
   310 \begin{mldecls}
   311     \indexdef{}{ML}{print\_mode\_value}\verb|print_mode_value: unit -> string list| \\
   312     \indexdef{}{ML}{Print\_Mode.with\_modes}\verb|Print_Mode.with_modes: string list -> ('a -> 'b) -> 'a -> 'b| \\
   313   \end{mldecls}
   314 
   315   The \emph{print mode} facility allows to modify various operations
   316   for printing.  Commands like \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}, \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}},
   317   \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}} (see \secref{sec:print-diag}) take additional print
   318   modes as optional argument.  The underlying ML operations are as
   319   follows.
   320 
   321   \begin{description}
   322 
   323   \item \verb|print_mode_value ()| yields the list of currently
   324   active print mode names.  This should be understood as symbolic
   325   representation of certain individual features for printing (with
   326   precedence from left to right).
   327 
   328   \item \verb|Print_Mode.with_modes|~\isa{{\isaliteral{22}{\isachardoublequote}}modes\ f\ x{\isaliteral{22}{\isachardoublequote}}} evaluates
   329   \isa{{\isaliteral{22}{\isachardoublequote}}f\ x{\isaliteral{22}{\isachardoublequote}}} in an execution context where the print mode is
   330   prepended by the given \isa{{\isaliteral{22}{\isachardoublequote}}modes{\isaliteral{22}{\isachardoublequote}}}.  This provides a thread-safe
   331   way to augment print modes.  It is also monotonic in the set of mode
   332   names: it retains the default print mode that certain
   333   user-interfaces might have installed for their proper functioning!
   334 
   335   \end{description}
   336 
   337   \begin{warn}
   338   The old global reference \verb|print_mode| should never be used
   339   directly in applications.  Its main reason for being publicly
   340   accessible is to support historic versions of Proof~General.
   341   \end{warn}
   342 
   343   \medskip The pretty printer for inner syntax maintains alternative
   344   mixfix productions for any print mode name invented by the user, say
   345   in commands like \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} or \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}.
   346   Mode names can be arbitrary, but the following ones have a specific
   347   meaning by convention:
   348 
   349   \begin{itemize}
   350 
   351   \item \verb|""| (the empty string): default mode;
   352   implicitly active as last element in the list of modes.
   353 
   354   \item \verb|input|: dummy print mode that is never active; may
   355   be used to specify notation that is only available for input.
   356 
   357   \item \verb|internal| dummy print mode that is never active;
   358   used internally in Isabelle/Pure.
   359 
   360   \item \verb|xsymbols|: enable proper mathematical symbols
   361   instead of ASCII art.\footnote{This traditional mode name stems from
   362   the ``X-Symbol'' package for old versions Proof~General with XEmacs,
   363   although that package has been superseded by Unicode in recent
   364   years.}
   365 
   366   \item \verb|HTML|: additional mode that is active in HTML
   367   presentation of Isabelle theory sources; allows to provide
   368   alternative output notation.
   369 
   370   \item \verb|latex|: additional mode that is active in {\LaTeX}
   371   document preparation of Isabelle theory sources; allows to provide
   372   alternative output notation.
   373 
   374   \end{itemize}%
   375 \end{isamarkuptext}%
   376 \isamarkuptrue%
   377 %
   378 \isamarkupsubsection{Printing limits%
   379 }
   380 \isamarkuptrue%
   381 %
   382 \begin{isamarkuptext}%
   383 \begin{mldecls}
   384     \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
   385     \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   386   \end{mldecls}
   387 
   388   These ML functions set limits for pretty printed text.
   389 
   390   \begin{description}
   391 
   392   \item \verb|Pretty.margin_default| indicates the global default for
   393   the right margin of the built-in pretty printer, with initial value
   394   76.  Note that user-interfaces typically control margins
   395   automatically when resizing windows, or even bypass the formatting
   396   engine of Isabelle/ML altogether and do it within the front end via
   397   Isabelle/Scala.
   398 
   399   \item \verb|print_depth|~\isa{n} limits the printing depth of the
   400   ML toplevel pretty printer; the precise effect depends on the ML
   401   compiler and run-time system.  Typically \isa{n} should be less
   402   than 10.  Bigger values such as 100--1000 are useful for debugging.
   403 
   404   \end{description}%
   405 \end{isamarkuptext}%
   406 \isamarkuptrue%
   407 %
   408 \isamarkupsection{Mixfix annotations \label{sec:mixfix}%
   409 }
   410 \isamarkuptrue%
   411 %
   412 \begin{isamarkuptext}%
   413 Mixfix annotations specify concrete \emph{inner syntax} of
   414   Isabelle types and terms.  Locally fixed parameters in toplevel
   415   theorem statements, locale and class specifications also admit
   416   mixfix annotations in a fairly uniform manner.  A mixfix annotation
   417   describes describes the concrete syntax, the translation to abstract
   418   syntax, and the pretty printing.  Special case annotations provide a
   419   simple means of specifying infix operators and binders.
   420 
   421   Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}.  It allows
   422   to specify any context-free priority grammar, which is more general
   423   than the fixity declarations of ML and Prolog.
   424 
   425   \begin{railoutput}
   426 \rail@begin{1}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
   427 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
   428 \rail@nont{\isa{mfix}}[]
   429 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   430 \rail@end
   431 \rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
   432 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
   433 \rail@bar
   434 \rail@nont{\isa{mfix}}[]
   435 \rail@nextbar{1}
   436 \rail@term{\isa{\isakeyword{structure}}}[]
   437 \rail@endbar
   438 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
   439 \rail@end
   440 \rail@begin{7}{\isa{mfix}}
   441 \rail@bar
   442 \rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
   443 \rail@bar
   444 \rail@nextbar{1}
   445 \rail@nont{\isa{prios}}[]
   446 \rail@endbar
   447 \rail@bar
   448 \rail@nextbar{1}
   449 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   450 \rail@endbar
   451 \rail@nextbar{2}
   452 \rail@bar
   453 \rail@term{\isa{\isakeyword{infix}}}[]
   454 \rail@nextbar{3}
   455 \rail@term{\isa{\isakeyword{infixl}}}[]
   456 \rail@nextbar{4}
   457 \rail@term{\isa{\isakeyword{infixr}}}[]
   458 \rail@endbar
   459 \rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
   460 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   461 \rail@nextbar{5}
   462 \rail@term{\isa{\isakeyword{binder}}}[]
   463 \rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
   464 \rail@bar
   465 \rail@nextbar{6}
   466 \rail@nont{\isa{prios}}[]
   467 \rail@endbar
   468 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   469 \rail@endbar
   470 \rail@end
   471 \rail@begin{1}{\isa{template}}
   472 \rail@nont{\isa{string}}[]
   473 \rail@end
   474 \rail@begin{2}{\isa{prios}}
   475 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
   476 \rail@plus
   477 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
   478 \rail@nextplus{1}
   479 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
   480 \rail@endplus
   481 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
   482 \rail@end
   483 \end{railoutput}
   484 
   485 
   486   The string given as \isa{template} may include literal text,
   487   spacing, blocks, and arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the
   488   special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'')
   489   represents an index argument that specifies an implicit structure
   490   reference (see also \secref{sec:locale}).  Infix and binder
   491   declarations provide common abbreviations for particular mixfix
   492   declarations.  So in practice, mixfix templates mostly degenerate to
   493   literal text for concrete syntax, such as ``\verb|++|'' for
   494   an infix symbol.%
   495 \end{isamarkuptext}%
   496 \isamarkuptrue%
   497 %
   498 \isamarkupsubsection{The general mixfix form%
   499 }
   500 \isamarkuptrue%
   501 %
   502 \begin{isamarkuptext}%
   503 In full generality, mixfix declarations work as follows.
   504   Suppose a constant \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} is annotated by
   505   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mixfix\ {\isaliteral{5B}{\isacharbrackleft}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}mixfix{\isaliteral{22}{\isachardoublequote}}} is a string
   506   \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} consisting of delimiters that surround
   507   argument positions as indicated by underscores.
   508 
   509   Altogether this determines a production for a context-free priority
   510   grammar, where for each argument \isa{{\isaliteral{22}{\isachardoublequote}}i{\isaliteral{22}{\isachardoublequote}}} the syntactic category
   511   is determined by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} (with priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}), and the
   512   result category is determined from \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} (with priority \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}).  Priority specifications are optional, with default 0 for
   513   arguments and 1000 for the result.\footnote{Omitting priorities is
   514   prone to syntactic ambiguities unless the delimiter tokens determine
   515   fully bracketed notation, as in \isa{{\isaliteral{22}{\isachardoublequote}}if\ {\isaliteral{5F}{\isacharunderscore}}\ then\ {\isaliteral{5F}{\isacharunderscore}}\ else\ {\isaliteral{5F}{\isacharunderscore}}\ fi{\isaliteral{22}{\isachardoublequote}}}.}
   516 
   517   Since \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} may be again a function type, the constant
   518   type scheme may have more argument positions than the mixfix
   519   pattern.  Printing a nested application \isa{{\isaliteral{22}{\isachardoublequote}}c\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}} for
   520   \isa{{\isaliteral{22}{\isachardoublequote}}m\ {\isaliteral{3E}{\isachargreater}}\ n{\isaliteral{22}{\isachardoublequote}}} works by attaching concrete notation only to the
   521   innermost part, essentially by printing \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}c\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}
   522   instead.  If a term has fewer arguments than specified in the mixfix
   523   template, the concrete syntax is ignored.
   524 
   525   \medskip A mixfix template may also contain additional directives
   526   for pretty printing, notably spaces, blocks, and breaks.  The
   527   general template format is a sequence over any of the following
   528   entities.
   529 
   530   \begin{description}
   531 
   532   \item \isa{{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}} is a delimiter, namely a non-empty sequence of
   533   characters other than the following special characters:
   534 
   535   \smallskip
   536   \begin{tabular}{ll}
   537     \verb|'| & single quote \\
   538     \verb|_| & underscore \\
   539     \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} & index symbol \\
   540     \verb|(| & open parenthesis \\
   541     \verb|)| & close parenthesis \\
   542     \verb|/| & slash \\
   543   \end{tabular}
   544   \medskip
   545 
   546   \item \verb|'| escapes the special meaning of these
   547   meta-characters, producing a literal version of the following
   548   character, unless that is a blank.
   549 
   550   A single quote followed by a blank separates delimiters, without
   551   affecting printing, but input tokens may have additional white space
   552   here.
   553 
   554   \item \verb|_| is an argument position, which stands for a
   555   certain syntactic category in the underlying grammar.
   556 
   557   \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} is an indexed argument position; this is the place
   558   where implicit structure arguments can be attached.
   559 
   560   \item \isa{{\isaliteral{22}{\isachardoublequote}}s{\isaliteral{22}{\isachardoublequote}}} is a non-empty sequence of spaces for printing.
   561   This and the following specifications do not affect parsing at all.
   562 
   563   \item \verb|(|\isa{n} opens a pretty printing block.  The
   564   optional number specifies how much indentation to add when a line
   565   break occurs within the block.  If the parenthesis is not followed
   566   by digits, the indentation defaults to 0.  A block specified via
   567   \verb|(00| is unbreakable.
   568 
   569   \item \verb|)| closes a pretty printing block.
   570 
   571   \item \verb|//| forces a line break.
   572 
   573   \item \verb|/|\isa{s} allows a line break.  Here \isa{s}
   574   stands for the string of spaces (zero or more) right after the
   575   slash.  These spaces are printed if the break is \emph{not} taken.
   576 
   577   \end{description}
   578 
   579   The general idea of pretty printing with blocks and breaks is also
   580   described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.%
   581 \end{isamarkuptext}%
   582 \isamarkuptrue%
   583 %
   584 \isamarkupsubsection{Infixes%
   585 }
   586 \isamarkuptrue%
   587 %
   588 \begin{isamarkuptext}%
   589 Infix operators are specified by convenient short forms that
   590   abbreviate general mixfix annotations as follows:
   591 
   592   \begin{center}
   593   \begin{tabular}{lll}
   594 
   595   \verb|(|\indexdef{}{keyword}{infix}\hypertarget{keyword.infix}{\hyperlink{keyword.infix}{\mbox{\isa{\isakeyword{infix}}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
   596   & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
   597   \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
   598   \verb|(|\indexdef{}{keyword}{infixl}\hypertarget{keyword.infixl}{\hyperlink{keyword.infixl}{\mbox{\isa{\isakeyword{infixl}}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
   599   & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
   600   \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
   601   \verb|(|\indexdef{}{keyword}{infixr}\hypertarget{keyword.infixr}{\hyperlink{keyword.infixr}{\mbox{\isa{\isakeyword{infixr}}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
   602   & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
   603   \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
   604 
   605   \end{tabular}
   606   \end{center}
   607 
   608   The mixfix template \verb|"(_ |\isa{sy}\verb|/ _)"|
   609   specifies two argument positions; the delimiter is preceded by a
   610   space and followed by a space or line break; the entire phrase is a
   611   pretty printing block.
   612 
   613   The alternative notation \verb|op|~\isa{sy} is introduced
   614   in addition.  Thus any infix operator may be written in prefix form
   615   (as in ML), independently of the number of arguments in the term.%
   616 \end{isamarkuptext}%
   617 \isamarkuptrue%
   618 %
   619 \isamarkupsubsection{Binders%
   620 }
   621 \isamarkuptrue%
   622 %
   623 \begin{isamarkuptext}%
   624 A \emph{binder} is a variable-binding construct such as a
   625   quantifier.  The idea to formalize \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}} as \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} for \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequote}}} already goes back
   626   to \cite{church40}.  Isabelle declarations of certain higher-order
   627   operators may be annotated with \indexdef{}{keyword}{binder}\hypertarget{keyword.binder}{\hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}}} annotations
   628   as follows:
   629 
   630   \begin{center}
   631   \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|"  (|\hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}}\verb| "|\isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}\verb|" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)|
   632   \end{center}
   633 
   634   This introduces concrete binder syntax \isa{{\isaliteral{22}{\isachardoublequote}}sy\ x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}}, where
   635   \isa{x} is a bound variable of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, the body \isa{b} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} and the whole term has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}.
   636   The optional integer \isa{p} specifies the syntactic priority of
   637   the body; the default is \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}, which is also the priority of
   638   the whole construct.
   639 
   640   Internally, the binder syntax is expanded to something like this:
   641   \begin{center}
   642   \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}idts\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|"  ("(3|\isa{sy}\verb|_./ _)" [0, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)|
   643   \end{center}
   644 
   645   Here \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} is the nonterminal symbol for a list of
   646   identifiers with optional type constraints (see also
   647   \secref{sec:pure-grammar}).  The mixfix template \verb|"(3|\isa{sy}\verb|_./ _)"| defines argument positions
   648   for the bound identifiers and the body, separated by a dot with
   649   optional line break; the entire phrase is a pretty printing block of
   650   indentation level 3.  Note that there is no extra space after \isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}, so it needs to be included user specification if the binder
   651   syntax ends with a token that may be continued by an identifier
   652   token at the start of \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}.
   653 
   654   Furthermore, a syntax translation to transforms \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ b{\isaliteral{22}{\isachardoublequote}}} into iterated application \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
   655   This works in both directions, for parsing and printing.%
   656 \end{isamarkuptext}%
   657 \isamarkuptrue%
   658 %
   659 \isamarkupsection{Explicit notation \label{sec:notation}%
   660 }
   661 \isamarkuptrue%
   662 %
   663 \begin{isamarkuptext}%
   664 \begin{matharray}{rcll}
   665     \indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
   666     \indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{5F}{\isacharunderscore}}notation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
   667     \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
   668     \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}notation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
   669     \indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   670   \end{matharray}
   671 
   672   Commands that introduce new logical entities (terms or types)
   673   usually allow to provide mixfix annotations on the spot, which is
   674   convenient for default notation.  Nonetheless, the syntax may be
   675   modified later on by declarations for explicit notation.  This
   676   allows to add or delete mixfix annotations for of existing logical
   677   entities within the current context.
   678 
   679   \begin{railoutput}
   680 \rail@begin{5}{}
   681 \rail@bar
   682 \rail@term{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
   683 \rail@nextbar{1}
   684 \rail@term{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
   685 \rail@endbar
   686 \rail@bar
   687 \rail@nextbar{1}
   688 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
   689 \rail@endbar
   690 \rail@bar
   691 \rail@nextbar{1}
   692 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
   693 \rail@endbar
   694 \rail@cr{3}
   695 \rail@plus
   696 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   697 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
   698 \rail@nextplus{4}
   699 \rail@cterm{\isa{\isakeyword{and}}}[]
   700 \rail@endplus
   701 \rail@end
   702 \rail@begin{5}{}
   703 \rail@bar
   704 \rail@term{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}}[]
   705 \rail@nextbar{1}
   706 \rail@term{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}notation}}}}}[]
   707 \rail@endbar
   708 \rail@bar
   709 \rail@nextbar{1}
   710 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
   711 \rail@endbar
   712 \rail@bar
   713 \rail@nextbar{1}
   714 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
   715 \rail@endbar
   716 \rail@cr{3}
   717 \rail@plus
   718 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   719 \rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
   720 \rail@nextplus{4}
   721 \rail@cterm{\isa{\isakeyword{and}}}[]
   722 \rail@endplus
   723 \rail@end
   724 \rail@begin{2}{}
   725 \rail@term{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}}[]
   726 \rail@bar
   727 \rail@nextbar{1}
   728 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
   729 \rail@endbar
   730 \rail@plus
   731 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
   732 \rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
   733 \rail@nextplus{1}
   734 \rail@cterm{\isa{\isakeyword{and}}}[]
   735 \rail@endplus
   736 \rail@end
   737 \end{railoutput}
   738 
   739 
   740   \begin{description}
   741 
   742   \item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} associates mixfix
   743   syntax with an existing type constructor.  The arity of the
   744   constructor is retrieved from the context.
   745 
   746   \item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}type{\isaliteral{5F}{\isacharunderscore}}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}notation}}}}, but removes the specified syntax annotation from
   747   the present context.
   748 
   749   \item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} associates mixfix
   750   syntax with an existing constant or fixed variable.  The type
   751   declaration of the given entity is retrieved from the context.
   752 
   753   \item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}},
   754   but removes the specified syntax annotation from the present
   755   context.
   756 
   757   \item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but
   758   works within an Isar proof body.
   759 
   760   \end{description}%
   761 \end{isamarkuptext}%
   762 \isamarkuptrue%
   763 %
   764 \isamarkupsection{The Pure syntax \label{sec:pure-syntax}%
   765 }
   766 \isamarkuptrue%
   767 %
   768 \isamarkupsubsection{Lexical matters \label{sec:inner-lex}%
   769 }
   770 \isamarkuptrue%
   771 %
   772 \begin{isamarkuptext}%
   773 The inner lexical syntax vaguely resembles the outer one
   774   (\secref{sec:outer-lex}), but some details are different.  There are
   775   two main categories of inner syntax tokens:
   776 
   777   \begin{enumerate}
   778 
   779   \item \emph{delimiters} --- the literal tokens occurring in
   780   productions of the given priority grammar (cf.\
   781   \secref{sec:priority-grammar});
   782 
   783   \item \emph{named tokens} --- various categories of identifiers etc.
   784 
   785   \end{enumerate}
   786 
   787   Delimiters override named tokens and may thus render certain
   788   identifiers inaccessible.  Sometimes the logical context admits
   789   alternative ways to refer to the same entity, potentially via
   790   qualified names.
   791 
   792   \medskip The categories for named tokens are defined once and for
   793   all as follows, reusing some categories of the outer token syntax
   794   (\secref{sec:outer-lex}).
   795 
   796   \begin{center}
   797   \begin{supertabular}{rcl}
   798     \indexdef{inner}{syntax}{id}\hypertarget{syntax.inner.id}{\hyperlink{syntax.inner.id}{\mbox{\isa{id}}}} & = & \indexref{}{syntax}{ident}\hyperlink{syntax.ident}{\mbox{\isa{ident}}} \\
   799     \indexdef{inner}{syntax}{longid}\hypertarget{syntax.inner.longid}{\hyperlink{syntax.inner.longid}{\mbox{\isa{longid}}}} & = & \indexref{}{syntax}{longident}\hyperlink{syntax.longident}{\mbox{\isa{longident}}} \\
   800     \indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\
   801     \indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\
   802     \indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\
   803     \indexdef{inner}{syntax}{num\_token}\hypertarget{syntax.inner.num-token}{\hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
   804     \indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
   805     \indexdef{inner}{syntax}{xnum\_token}\hypertarget{syntax.inner.xnum-token}{\hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\
   806 
   807     \indexdef{inner}{syntax}{str\_token}\hypertarget{syntax.inner.str-token}{\hyperlink{syntax.inner.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}}} & = & \verb|''| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|''| \\
   808   \end{supertabular}
   809   \end{center}
   810 
   811   The token categories \hyperlink{syntax.inner.num-token}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}token}}}, \hyperlink{syntax.inner.xnum-token}{\mbox{\isa{xnum{\isaliteral{5F}{\isacharunderscore}}token}}}, and \hyperlink{syntax.inner.str-token}{\mbox{\isa{str{\isaliteral{5F}{\isacharunderscore}}token}}} are not used in Pure.  Object-logics may implement numerals
   812   and string constants by adding appropriate syntax declarations,
   813   together with some translation functions (e.g.\ see Isabelle/HOL).
   814 
   815   The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}}, \indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isaliteral{5F}{\isacharunderscore}}const}}}}, and \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isaliteral{5F}{\isacharunderscore}}const}}}} provide
   816   robust access to the respective tokens: the syntax tree holds a
   817   syntactic constant instead of a free variable.%
   818 \end{isamarkuptext}%
   819 \isamarkuptrue%
   820 %
   821 \isamarkupsubsection{Priority grammars \label{sec:priority-grammar}%
   822 }
   823 \isamarkuptrue%
   824 %
   825 \begin{isamarkuptext}%
   826 A context-free grammar consists of a set of \emph{terminal
   827   symbols}, a set of \emph{nonterminal symbols} and a set of
   828   \emph{productions}.  Productions have the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{22}{\isachardoublequote}}},
   829   where \isa{A} is a nonterminal and \isa{{\isaliteral{5C3C67616D6D613E}{\isasymgamma}}} is a string of
   830   terminals and nonterminals.  One designated nonterminal is called
   831   the \emph{root symbol}.  The language defined by the grammar
   832   consists of all strings of terminals that can be derived from the
   833   root symbol by applying productions as rewrite rules.
   834 
   835   The standard Isabelle parser for inner syntax uses a \emph{priority
   836   grammar}.  Each nonterminal is decorated by an integer priority:
   837   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup p\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.  In a derivation, \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup p\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} may be rewritten
   838   using a production \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup q\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{22}{\isachardoublequote}}} only if \isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{5C3C6C653E}{\isasymle}}\ q{\isaliteral{22}{\isachardoublequote}}}.  Any
   839   priority grammar can be translated into a normal context-free
   840   grammar by introducing new nonterminals and productions.
   841 
   842   \medskip Formally, a set of context free productions \isa{G}
   843   induces a derivation relation \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub G{\isaliteral{22}{\isachardoublequote}}} as follows.  Let \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} and \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}} denote strings of terminal or nonterminal symbols.
   844   Then \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup p\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub G\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequote}}} holds if and only if \isa{G}
   845   contains some production \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup q\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C67616D6D613E}{\isasymgamma}}{\isaliteral{22}{\isachardoublequote}}} for \isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{5C3C6C653E}{\isasymle}}\ q{\isaliteral{22}{\isachardoublequote}}}.
   846 
   847   \medskip The following grammar for arithmetic expressions
   848   demonstrates how binding power and associativity of operators can be
   849   enforced by priorities.
   850 
   851   \begin{center}
   852   \begin{tabular}{rclr}
   853   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|)| \\
   854   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \verb|0| \\
   855   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|+| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   856   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|*| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   857   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \verb|-| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   858   \end{tabular}
   859   \end{center}
   860   The choice of priorities determines that \verb|-| binds
   861   tighter than \verb|*|, which binds tighter than \verb|+|.  Furthermore \verb|+| associates to the left and
   862   \verb|*| to the right.
   863 
   864   \medskip For clarity, grammars obey these conventions:
   865   \begin{itemize}
   866 
   867   \item All priorities must lie between 0 and 1000.
   868 
   869   \item Priority 0 on the right-hand side and priority 1000 on the
   870   left-hand side may be omitted.
   871 
   872   \item The production \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup p\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} is written as \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, i.e.\ the priority of the left-hand side actually appears in
   873   a column on the far right.
   874 
   875   \item Alternatives are separated by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}}.
   876 
   877   \item Repetition is indicated by dots \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} in an informal
   878   but obvious way.
   879 
   880   \end{itemize}
   881 
   882   Using these conventions, the example grammar specification above
   883   takes the form:
   884   \begin{center}
   885   \begin{tabular}{rclc}
   886     \isa{A} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{A} \verb|)| \\
   887               & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|0| & \qquad\qquad \\
   888               & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{A} \verb|+| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   889               & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|*| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   890               & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|-| \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   891   \end{tabular}
   892   \end{center}%
   893 \end{isamarkuptext}%
   894 \isamarkuptrue%
   895 %
   896 \isamarkupsubsection{The Pure grammar \label{sec:pure-grammar}%
   897 }
   898 \isamarkuptrue%
   899 %
   900 \begin{isamarkuptext}%
   901 The priority grammar of the \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} theory is defined
   902   approximately like this:
   903 
   904   \begin{center}
   905   \begin{supertabular}{rclr}
   906 
   907   \indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}prop\ \ {\isaliteral{7C}{\isacharbar}}\ \ logic{\isaliteral{22}{\isachardoublequote}}} \\\\
   908 
   909   \indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\
   910     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{4}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   911     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|==| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   912     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   913     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|&&&| \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   914     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|==>| \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   915     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{2}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   916     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[|\verb,|,\verb|| \isa{prop} \verb|;| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|;| \isa{prop} \verb||\verb,|,\verb|]| \verb|==>| \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   917     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{22}{\isachardoublequote}}} \isa{prop} \verb|;| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|;| \isa{prop} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}prop\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   918     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|!!| \isa{idts} \verb|.| \isa{prop} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   919     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   920     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\
   921     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\
   922     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|TERM| \isa{logic} \\
   923     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|PROP| \isa{aprop} \\\\
   924 
   925   \indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\
   926     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ var\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|...| \\
   927     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
   928     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
   929     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ \ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
   930 
   931   \indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\
   932     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{4}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   933     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ var\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|...| \\
   934     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
   935     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
   936     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ \ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   937     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7374727563743E}{\isasymstruct}}\ index\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   938     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   939     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} \isa{pttrns} \verb|.| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   940     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|op| \verb|==|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \verb|&&&| \\
   941     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|op| \verb|==>|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
   942     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\
   943 
   944   \indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \\
   945     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{id} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   946     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|_| \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
   947 
   948   \indexdef{inner}{syntax}{index}\hypertarget{syntax.inner.index}{\hyperlink{syntax.inner.index}{\mbox{\isa{index}}}} & = & \verb|\<^bsub>| \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|\<^esub>|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} \\\\
   949 
   950   \indexdef{inner}{syntax}{idts}\hypertarget{syntax.inner.idts}{\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}idt\ \ {\isaliteral{7C}{\isacharbar}}\ \ idt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ idts{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
   951 
   952   \indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\
   953 
   954   \indexdef{inner}{syntax}{pttrns}\hypertarget{syntax.inner.pttrns}{\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}pttrn\ \ {\isaliteral{7C}{\isacharbar}}\ \ pttrn\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ pttrns{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
   955 
   956   \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
   957     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}tid\ \ {\isaliteral{7C}{\isacharbar}}\ \ tvar\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \\
   958     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}tid{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort\ \ {\isaliteral{7C}{\isacharbar}}\ \ tvar\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort{\isaliteral{22}{\isachardoublequote}}} \\
   959     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{5F}{\isacharunderscore}}name\ \ {\isaliteral{7C}{\isacharbar}}\ \ type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ type{\isaliteral{5F}{\isacharunderscore}}name{\isaliteral{22}{\isachardoublequote}}} \\
   960     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|)| \isa{type{\isaliteral{5F}{\isacharunderscore}}name} \\
   961     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|=>| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   962     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   963     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   964     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|]| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
   965   \indexdef{inner}{syntax}{type\_name}\hypertarget{syntax.inner.type-name}{\hyperlink{syntax.inner.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid{\isaliteral{22}{\isachardoublequote}}} \\\\
   966 
   967   \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}}~\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|{}| \\
   968     & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|{| \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}} \verb|}| \\
   969   \indexdef{inner}{syntax}{class\_name}\hypertarget{syntax.inner.class-name}{\hyperlink{syntax.inner.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid{\isaliteral{22}{\isachardoublequote}}} \\
   970   \end{supertabular}
   971   \end{center}
   972 
   973   \medskip Here literal terminals are printed \verb|verbatim|;
   974   see also \secref{sec:inner-lex} for further token categories of the
   975   inner syntax.  The meaning of the nonterminals defined by the above
   976   grammar is as follows:
   977 
   978   \begin{description}
   979 
   980   \item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term.
   981 
   982   \item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions,
   983   which are terms of type \isa{prop}.  The syntax of such formulae of
   984   the meta-logic is carefully distinguished from usual conventions for
   985   object-logics.  In particular, plain \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}}-term notation is
   986   \emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
   987 
   988   \item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which
   989   are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an
   990   explicit \verb|PROP| token.
   991 
   992   Terms of type \isa{prop} with non-constant head, e.g.\ a plain
   993   variable, are printed in this form.  Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise
   994   the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and
   995   cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}.
   996 
   997   \item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a
   998   logical type, excluding type \isa{prop}.  This is the main
   999   syntactic category of object-logic entities, covering plain \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-term notation (variables, abstraction, application), plus
  1000   anything defined by the user.
  1001 
  1002   When specifying notation for logical entities, all logical types
  1003   (excluding \isa{prop}) are \emph{collapsed} to this single category
  1004   of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}.
  1005 
  1006   \item \indexref{inner}{syntax}{index}\hyperlink{syntax.inner.index}{\mbox{\isa{index}}} denotes an optional index term for
  1007   indexed syntax.  If omitted, it refers to the first \hyperlink{keyword.structure}{\mbox{\isa{\isakeyword{structure}}}} variable in the context.  The special dummy ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'' serves as pattern variable in mixfix annotations that
  1008   introduce indexed notation.
  1009 
  1010   \item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly
  1011   constrained by types.
  1012 
  1013   \item \indexref{inner}{syntax}{idts}\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} denotes a sequence of \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}.  This is the most basic category for variables in
  1014   iterated binders, such as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{22}{\isachardoublequote}}} or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}}.
  1015 
  1016   \item \indexref{inner}{syntax}{pttrn}\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}} and \indexref{inner}{syntax}{pttrns}\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}
  1017   denote patterns for abstraction, cases bindings etc.  In Pure, these
  1018   categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and
  1019   \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively.  Object-logics may add
  1020   additional productions for binding forms.
  1021 
  1022   \item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic.
  1023 
  1024   \item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts.
  1025 
  1026   \end{description}
  1027 
  1028   Here are some further explanations of certain syntax features.
  1029 
  1030   \begin{itemize}
  1031 
  1032   \item In \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, note that \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ y{\isaliteral{22}{\isachardoublequote}}} is
  1033   parsed as \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}nat\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, treating \isa{y} like a type
  1034   constructor applied to \isa{nat}.  To avoid this interpretation,
  1035   write \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ y{\isaliteral{22}{\isachardoublequote}}} with explicit parentheses.
  1036 
  1037   \item Similarly, \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{22}{\isachardoublequote}}} is parsed as \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}nat\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.  The correct form is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, or \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{22}{\isachardoublequote}}} if \isa{y} is last in the
  1038   sequence of identifiers.
  1039 
  1040   \item Type constraints for terms bind very weakly.  For example,
  1041   \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3C}{\isacharless}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{22}{\isachardoublequote}}} is normally parsed as \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3C}{\isacharless}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{22}{\isachardoublequote}}}, unless \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} has a very low priority, in which case the
  1042   input is likely to be ambiguous.  The correct form is \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
  1043 
  1044   \item Constraints may be either written with two literal colons
  1045   ``\verb|::|'' or the double-colon symbol \verb|\<Colon>|,
  1046   which actually looks exactly the same in some {\LaTeX} styles.
  1047 
  1048   \item Dummy variables (written as underscore) may occur in different
  1049   roles.
  1050 
  1051   \begin{description}
  1052 
  1053   \item A type ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' or ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ sort{\isaliteral{22}{\isachardoublequote}}}'' acts like an
  1054   anonymous inference parameter, which is filled-in according to the
  1055   most general type produced by the type-checking phase.
  1056 
  1057   \item A bound ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' refers to a vacuous abstraction, where
  1058   the body does not refer to the binding introduced here.  As in the
  1059   term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequote}}}, which is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}}-equivalent to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequote}}}.
  1060 
  1061   \item A free ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' refers to an implicit outer binding.
  1062   Higher definitional packages usually allow forms like \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequote}}}.
  1063 
  1064   \item A schematic ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'' (within a term pattern, see
  1065   \secref{sec:term-decls}) refers to an anonymous variable that is
  1066   implicitly abstracted over its context of locally bound variables.
  1067   For example, this allows pattern matching of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} against \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, or even \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} by
  1068   using both bound and schematic dummies.
  1069 
  1070   \end{description}
  1071 
  1072   \item The three literal dots ``\verb|...|'' may be also
  1073   written as ellipsis symbol \verb|\<dots>|.  In both cases this
  1074   refers to a special schematic variable, which is bound in the
  1075   context.  This special term abbreviation works nicely with
  1076   calculational reasoning (\secref{sec:calculation}).
  1077 
  1078   \item \verb|CONST| ensures that the given identifier is treated
  1079   as constant term, and passed through the parse tree in fully
  1080   internalized form.  This is particularly relevant for translation
  1081   rules (\secref{sec:syn-trans}), notably on the RHS.
  1082 
  1083   \item \verb|XCONST| is similar to \verb|CONST|, but
  1084   retains the constant name as given.  This is only relevant to
  1085   translation rules (\secref{sec:syn-trans}), notably on the LHS.
  1086 
  1087   \end{itemize}%
  1088 \end{isamarkuptext}%
  1089 \isamarkuptrue%
  1090 %
  1091 \isamarkupsubsection{Inspecting the syntax%
  1092 }
  1093 \isamarkuptrue%
  1094 %
  1095 \begin{isamarkuptext}%
  1096 \begin{matharray}{rcl}
  1097     \indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  1098   \end{matharray}
  1099 
  1100   \begin{description}
  1101 
  1102   \item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}syntax}}}} prints the inner syntax of the
  1103   current context.  The output can be quite large; the most important
  1104   sections are explained below.
  1105 
  1106   \begin{description}
  1107 
  1108   \item \isa{{\isaliteral{22}{\isachardoublequote}}lexicon{\isaliteral{22}{\isachardoublequote}}} lists the delimiters of the inner token
  1109   language; see \secref{sec:inner-lex}.
  1110 
  1111   \item \isa{{\isaliteral{22}{\isachardoublequote}}prods{\isaliteral{22}{\isachardoublequote}}} lists the productions of the underlying
  1112   priority grammar; see \secref{sec:priority-grammar}.
  1113 
  1114   The nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup p\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is rendered in plain text as \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{5B}{\isacharbrackleft}}p{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}; delimiters are quoted.  Many productions have an extra
  1115   \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ name{\isaliteral{22}{\isachardoublequote}}}.  These names later become the heads of parse
  1116   trees; they also guide the pretty printer.
  1117 
  1118   Productions without such parse tree names are called \emph{copy
  1119   productions}.  Their right-hand side must have exactly one
  1120   nonterminal symbol (or named token).  The parser does not create a
  1121   new parse tree node for copy productions, but simply returns the
  1122   parse tree of the right-hand symbol.
  1123 
  1124   If the right-hand side of a copy production consists of a single
  1125   nonterminal without any delimiters, then it is called a \emph{chain
  1126   production}.  Chain productions act as abbreviations: conceptually,
  1127   they are removed from the grammar by adding new productions.
  1128   Priority information attached to chain productions is ignored; only
  1129   the dummy value \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} is displayed.
  1130 
  1131   \item \isa{{\isaliteral{22}{\isachardoublequote}}print\ modes{\isaliteral{22}{\isachardoublequote}}} lists the alternative print modes
  1132   provided by this grammar; see \secref{sec:print-modes}.
  1133 
  1134   \item \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}rules{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}print{\isaliteral{5F}{\isacharunderscore}}rules{\isaliteral{22}{\isachardoublequote}}} relate to
  1135   syntax translations (macros); see \secref{sec:syn-trans}.
  1136 
  1137   \item \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} list sets of constants that invoke
  1138   translation functions for abstract syntax trees, which are only
  1139   required in very special situations; see \secref{sec:tr-funs}.
  1140 
  1141   \item \isa{{\isaliteral{22}{\isachardoublequote}}parse{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}print{\isaliteral{5F}{\isacharunderscore}}translation{\isaliteral{22}{\isachardoublequote}}}
  1142   list the sets of constants that invoke regular translation
  1143   functions; see \secref{sec:tr-funs}.
  1144 
  1145   \end{description}
  1146 
  1147   \end{description}%
  1148 \end{isamarkuptext}%
  1149 \isamarkuptrue%
  1150 %
  1151 \isamarkupsubsection{Ambiguity of parsed expressions%
  1152 }
  1153 \isamarkuptrue%
  1154 %
  1155 \begin{isamarkuptext}%
  1156 \begin{tabular}{rcll}
  1157     \indexdef{}{attribute}{syntax\_ambiguity\_warning}\hypertarget{attribute.syntax-ambiguity-warning}{\hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}}} & : & \isa{attribute} & default \isa{true} \\
  1158     \indexdef{}{attribute}{syntax\_ambiguity\_limit}\hypertarget{attribute.syntax-ambiguity-limit}{\hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
  1159   \end{tabular}
  1160 
  1161   Depending on the grammar and the given input, parsing may be
  1162   ambiguous.  Isabelle lets the Earley parser enumerate all possible
  1163   parse trees, and then tries to make the best out of the situation.
  1164   Terms that cannot be type-checked are filtered out, which often
  1165   leads to a unique result in the end.  Unlike regular type
  1166   reconstruction, which is applied to the whole collection of input
  1167   terms simultaneously, the filtering stage only treats each given
  1168   term in isolation.  Filtering is also not attempted for individual
  1169   types or raw ASTs (as required for \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}).
  1170 
  1171   Certain warning or error messages are printed, depending on the
  1172   situation and the given configuration options.  Parsing ultimately
  1173   fails, if multiple results remain after the filtering phase.
  1174 
  1175   \begin{description}
  1176 
  1177   \item \hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}} controls output of
  1178   explicit warning messages about syntax ambiguity.
  1179 
  1180   \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of
  1181   resulting parse trees that are shown as part of the printed message
  1182   in case of an ambiguity.
  1183 
  1184   \end{description}%
  1185 \end{isamarkuptext}%
  1186 \isamarkuptrue%
  1187 %
  1188 \isamarkupsection{Raw syntax and translations \label{sec:syn-trans}%
  1189 }
  1190 \isamarkuptrue%
  1191 %
  1192 \begin{isamarkuptext}%
  1193 \begin{matharray}{rcl}
  1194     \indexdef{}{command}{nonterminal}\hypertarget{command.nonterminal}{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1195     \indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1196     \indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1197     \indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1198     \indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1199   \end{matharray}
  1200 
  1201   Unlike mixfix notation for existing formal entities
  1202   (\secref{sec:notation}), raw syntax declarations provide full access
  1203   to the priority grammar of the inner syntax.  This includes
  1204   additional syntactic categories (via \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}) and
  1205   free-form grammar productions (via \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}).  Additional
  1206   syntax translations (or macros, via \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}) are
  1207   required to turn resulting parse trees into proper representations
  1208   of formal entities again.
  1209 
  1210   \begin{railoutput}
  1211 \rail@begin{2}{}
  1212 \rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[]
  1213 \rail@plus
  1214 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1215 \rail@nextplus{1}
  1216 \rail@cterm{\isa{\isakeyword{and}}}[]
  1217 \rail@endplus
  1218 \rail@end
  1219 \rail@begin{2}{}
  1220 \rail@bar
  1221 \rail@term{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}}[]
  1222 \rail@nextbar{1}
  1223 \rail@term{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}}[]
  1224 \rail@endbar
  1225 \rail@bar
  1226 \rail@nextbar{1}
  1227 \rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
  1228 \rail@endbar
  1229 \rail@plus
  1230 \rail@nont{\isa{constdecl}}[]
  1231 \rail@nextplus{1}
  1232 \rail@endplus
  1233 \rail@end
  1234 \rail@begin{7}{}
  1235 \rail@bar
  1236 \rail@term{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}}[]
  1237 \rail@nextbar{1}
  1238 \rail@term{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}}[]
  1239 \rail@endbar
  1240 \rail@plus
  1241 \rail@nont{\isa{transpat}}[]
  1242 \rail@bar
  1243 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}}}[]
  1244 \rail@nextbar{1}
  1245 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}}}[]
  1246 \rail@nextbar{2}
  1247 \rail@term{\isa{{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}}}[]
  1248 \rail@nextbar{3}
  1249 \rail@term{\isa{{\isaliteral{5C3C72696768746C656674686172706F6F6E733E}{\isasymrightleftharpoons}}}}[]
  1250 \rail@nextbar{4}
  1251 \rail@term{\isa{{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}}}[]
  1252 \rail@nextbar{5}
  1253 \rail@term{\isa{{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}}}[]
  1254 \rail@endbar
  1255 \rail@nont{\isa{transpat}}[]
  1256 \rail@nextplus{6}
  1257 \rail@endplus
  1258 \rail@end
  1259 \rail@begin{2}{\isa{constdecl}}
  1260 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1261 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
  1262 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
  1263 \rail@bar
  1264 \rail@nextbar{1}
  1265 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
  1266 \rail@endbar
  1267 \rail@end
  1268 \rail@begin{3}{\isa{mode}}
  1269 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1270 \rail@bar
  1271 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1272 \rail@nextbar{1}
  1273 \rail@term{\isa{\isakeyword{output}}}[]
  1274 \rail@nextbar{2}
  1275 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
  1276 \rail@term{\isa{\isakeyword{output}}}[]
  1277 \rail@endbar
  1278 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1279 \rail@end
  1280 \rail@begin{2}{\isa{transpat}}
  1281 \rail@bar
  1282 \rail@nextbar{1}
  1283 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1284 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
  1285 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1286 \rail@endbar
  1287 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
  1288 \rail@end
  1289 \end{railoutput}
  1290 
  1291 
  1292   \begin{description}
  1293 
  1294   \item \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}~\isa{c} declares a type
  1295   constructor \isa{c} (without arguments) to act as purely syntactic
  1296   type: a nonterminal symbol of the inner syntax.
  1297 
  1298   \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} augments the
  1299   priority grammar and the pretty printer table for the given print
  1300   mode (default \verb|""|). An optional keyword \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} means that only the pretty printer table is affected.
  1301 
  1302   Following \secref{sec:mixfix}, the mixfix annotation \isa{{\isaliteral{22}{\isachardoublequote}}mx\ {\isaliteral{3D}{\isacharequal}}\ template\ ps\ q{\isaliteral{22}{\isachardoublequote}}} together with type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and
  1303   specify a grammar production.  The \isa{template} contains
  1304   delimiter tokens that surround \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}} argument positions
  1305   (\verb|_|).  The latter correspond to nonterminal symbols
  1306   \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} derived from the argument types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} as
  1307   follows:
  1308   \begin{itemize}
  1309 
  1310   \item \isa{{\isaliteral{22}{\isachardoublequote}}prop{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ prop{\isaliteral{22}{\isachardoublequote}}}
  1311 
  1312   \item \isa{{\isaliteral{22}{\isachardoublequote}}logic{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for logical type
  1313   constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ prop{\isaliteral{22}{\isachardoublequote}}}
  1314 
  1315   \item \isa{any} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} for type variables
  1316 
  1317   \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}}
  1318   (syntactic type constructor)
  1319 
  1320   \end{itemize}
  1321 
  1322   Each \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is decorated by priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} from the
  1323   given list \isa{{\isaliteral{22}{\isachardoublequote}}ps{\isaliteral{22}{\isachardoublequote}}}; misssing priorities default to 0.
  1324 
  1325   The resulting nonterminal of the production is determined similarly
  1326   from type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}, with priority \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}} and default 1000.
  1327 
  1328   \medskip Parsing via this production produces parse trees \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} for the argument slots.  The resulting parse tree is
  1329   composed as \isa{{\isaliteral{22}{\isachardoublequote}}c\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, by using the syntax constant \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} of the syntax declaration.
  1330 
  1331   Such syntactic constants are invented on the spot, without formal
  1332   check wrt.\ existing declarations.  It is conventional to use plain
  1333   identifiers prefixed by a single underscore (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}foobar{\isaliteral{22}{\isachardoublequote}}}).  Names should be chosen with care, to avoid clashes
  1334   with unrelated syntax declarations.
  1335 
  1336   \medskip The special case of copy production is specified by \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|""| (empty string).  It means that the
  1337   resulting parse tree \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is copied directly, without any
  1338   further decoration.
  1339 
  1340   \item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ decls{\isaliteral{22}{\isachardoublequote}}} removes grammar
  1341   declarations (and translations) resulting from \isa{decls}, which
  1342   are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above.
  1343 
  1344   \item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic
  1345   translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72696768746C656674686172706F6F6E733E}{\isasymrightleftharpoons}}{\isaliteral{22}{\isachardoublequote}}}),
  1346   parse rules (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7269676874686172706F6F6E75703E}{\isasymrightharpoonup}}{\isaliteral{22}{\isachardoublequote}}}), or print rules (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C656674686172706F6F6E646F776E3E}{\isasymleftharpoondown}}{\isaliteral{22}{\isachardoublequote}}}).
  1347   Translation patterns may be prefixed by the syntactic category to be
  1348   used for parsing; the default is \isa{logic}.
  1349 
  1350   \item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}~\isa{rules} removes syntactic
  1351   translation rules, which are interpreted in the same manner as for
  1352   \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above.
  1353 
  1354   \end{description}
  1355 
  1356   Raw syntax and translations provides a slightly more low-level
  1357   access to the grammar and the form of resulting parse trees.  It is
  1358   often possible to avoid this untyped macro mechanism, and use
  1359   type-safe \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} or \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}} instead.
  1360   Some important situations where \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} are really need are as follows:
  1361 
  1362   \begin{itemize}
  1363 
  1364   \item Iterated replacement via recursive \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}.
  1365   For example, consider list enumeration \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{2C}{\isacharcomma}}\ d{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as
  1366   defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
  1367 
  1368   \item Change of binding status of variables: anything beyond the
  1369   built-in \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} mixfix annotation requires explicit
  1370   syntax translations.  For example, consider list filter
  1371   comprehension \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}x\ {\isaliteral{5C3C6C6566746172726F773E}{\isasymleftarrow}}\ xs\ {\isaliteral{2E}{\isachardot}}\ P{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} as defined in theory \hyperlink{theory.List}{\mbox{\isa{List}}} in Isabelle/HOL.
  1372 
  1373   \end{itemize}%
  1374 \end{isamarkuptext}%
  1375 \isamarkuptrue%
  1376 %
  1377 \isamarkupsection{Syntax translation functions \label{sec:tr-funs}%
  1378 }
  1379 \isamarkuptrue%
  1380 %
  1381 \begin{isamarkuptext}%
  1382 \begin{matharray}{rcl}
  1383     \indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1384     \indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1385     \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1386     \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1387     \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
  1388   \end{matharray}
  1389 
  1390   \begin{railoutput}
  1391 \rail@begin{5}{}
  1392 \rail@bar
  1393 \rail@term{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
  1394 \rail@nextbar{1}
  1395 \rail@term{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
  1396 \rail@nextbar{2}
  1397 \rail@term{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
  1398 \rail@nextbar{3}
  1399 \rail@term{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
  1400 \rail@nextbar{4}
  1401 \rail@term{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}}[]
  1402 \rail@endbar
  1403 \rail@bar
  1404 \rail@nextbar{1}
  1405 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
  1406 \rail@term{\isa{\isakeyword{advanced}}}[]
  1407 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
  1408 \rail@endbar
  1409 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
  1410 \rail@end
  1411 \end{railoutput}
  1412 
  1413 
  1414   Syntax translation functions written in ML admit almost arbitrary
  1415   manipulations of Isabelle's inner syntax.  Any of the above commands
  1416   have a single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument that refers to an ML
  1417   expression of appropriate type, which are as follows by default:
  1418 
  1419 %FIXME proper antiquotations
  1420 \begin{ttbox}
  1421 val parse_ast_translation   : (string * (ast list -> ast)) list
  1422 val parse_translation       : (string * (term list -> term)) list
  1423 val print_translation       : (string * (term list -> term)) list
  1424 val typed_print_translation : (string * (typ -> term list -> term)) list
  1425 val print_ast_translation   : (string * (ast list -> ast)) list
  1426 \end{ttbox}
  1427 
  1428   If the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}advanced{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option is given, the corresponding
  1429   translation functions may depend on the current theory or proof
  1430   context.  This allows to implement advanced syntax mechanisms, as
  1431   translations functions may refer to specific theory declarations or
  1432   auxiliary proof data.
  1433 
  1434 %FIXME proper antiquotations
  1435 \begin{ttbox}
  1436 val parse_ast_translation:
  1437   (string * (Proof.context -> ast list -> ast)) list
  1438 val parse_translation:
  1439   (string * (Proof.context -> term list -> term)) list
  1440 val print_translation:
  1441   (string * (Proof.context -> term list -> term)) list
  1442 val typed_print_translation:
  1443   (string * (Proof.context -> typ -> term list -> term)) list
  1444 val print_ast_translation:
  1445   (string * (Proof.context -> ast list -> ast)) list
  1446 \end{ttbox}
  1447 
  1448   \medskip See also the chapter on ``Syntax Transformations'' in old
  1449   \cite{isabelle-ref} for further details on translations on parse
  1450   trees.%
  1451 \end{isamarkuptext}%
  1452 \isamarkuptrue%
  1453 %
  1454 \isadelimtheory
  1455 %
  1456 \endisadelimtheory
  1457 %
  1458 \isatagtheory
  1459 \isacommand{end}\isamarkupfalse%
  1460 %
  1461 \endisatagtheory
  1462 {\isafoldtheory}%
  1463 %
  1464 \isadelimtheory
  1465 %
  1466 \endisadelimtheory
  1467 \isanewline
  1468 \end{isabellebody}%
  1469 %%% Local Variables:
  1470 %%% mode: latex
  1471 %%% TeX-master: "root"
  1472 %%% End: