src/Doc/Isar_Ref/Outer_Syntax.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59785 4e6ab5831cc0
child 59853 4039d8aecda4
permissions -rw-r--r--
tuned signature;
     1 theory Outer_Syntax
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close>
     6 
     7 text \<open>
     8   The rather generic framework of Isabelle/Isar syntax emerges from
     9   three main syntactic categories: \emph{commands} of the top-level
    10   Isar engine (covering theory and proof elements), \emph{methods} for
    11   general goal refinements (analogous to traditional ``tactics''), and
    12   \emph{attributes} for operations on facts (within a certain
    13   context).  Subsequently we give a reference of basic syntactic
    14   entities underlying Isabelle/Isar syntax in a bottom-up manner.
    15   Concrete theory and proof language elements will be introduced later
    16   on.
    17 
    18   \medskip In order to get started with writing well-formed
    19   Isabelle/Isar documents, the most important aspect to be noted is
    20   the difference of \emph{inner} versus \emph{outer} syntax.  Inner
    21   syntax is that of Isabelle types and terms of the logic, while outer
    22   syntax is that of Isabelle/Isar theory sources (specifications and
    23   proofs).  As a general rule, inner syntax entities may occur only as
    24   \emph{atomic entities} within outer syntax.  For example, the string
    25   @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term
    26   specifications within a theory, while @{verbatim "x + y"} without
    27   quotes is not.
    28 
    29   Printed theory documents usually omit quotes to gain readability
    30   (this is a matter of {\LaTeX} macro setup, say via @{verbatim
    31   "\\isabellestyle"}, see also @{cite "isabelle-sys"}).  Experienced
    32   users of Isabelle/Isar may easily reconstruct the lost technical
    33   information, while mere readers need not care about quotes at all.
    34 \<close>
    35 
    36 
    37 section \<open>Commands\<close>
    38 
    39 text \<open>
    40   \begin{matharray}{rcl}
    41     @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    42     @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    43   \end{matharray}
    44 
    45   @{rail \<open>
    46     @@{command help} (@{syntax name} * )
    47   \<close>}
    48 
    49   \begin{description}
    50 
    51   \item @{command "print_commands"} prints all outer syntax keywords
    52   and commands.
    53 
    54   \item @{command "help"}~@{text "pats"} retrieves outer syntax
    55   commands according to the specified name patterns.
    56 
    57   \end{description}
    58 \<close>
    59 
    60 
    61 subsubsection \<open>Examples\<close>
    62 
    63 text \<open>Some common diagnostic commands are retrieved like this
    64   (according to usual naming conventions):\<close>
    65 
    66 help "print"
    67 help "find"
    68 
    69 
    70 section \<open>Lexical matters \label{sec:outer-lex}\<close>
    71 
    72 text \<open>The outer lexical syntax consists of three main categories of
    73   syntax tokens:
    74 
    75   \begin{enumerate}
    76 
    77   \item \emph{major keywords} --- the command names that are available
    78   in the present logic session;
    79 
    80   \item \emph{minor keywords} --- additional literal tokens required
    81   by the syntax of commands;
    82 
    83   \item \emph{named tokens} --- various categories of identifiers etc.
    84 
    85   \end{enumerate}
    86 
    87   Major keywords and minor keywords are guaranteed to be disjoint.
    88   This helps user-interfaces to determine the overall structure of a
    89   theory text, without knowing the full details of command syntax.
    90   Internally, there is some additional information about the kind of
    91   major keywords, which approximates the command type (theory command,
    92   proof command etc.).
    93 
    94   Keywords override named tokens.  For example, the presence of a
    95   command called @{verbatim term} inhibits the identifier @{verbatim
    96   term}, but the string @{verbatim \<open>"term"\<close>} can be used instead.
    97   By convention, the outer syntax always allows quoted strings in
    98   addition to identifiers, wherever a named entity is expected.
    99 
   100   When tokenizing a given input sequence, the lexer repeatedly takes
   101   the longest prefix of the input that forms a valid token.  Spaces,
   102   tabs, newlines and formfeeds between tokens serve as explicit
   103   separators.
   104 
   105   \medskip The categories for named tokens are defined once and for
   106   all as follows.
   107 
   108   \begin{center}
   109   \begin{supertabular}{rcl}
   110     @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
   111     @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
   112     @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
   113     @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
   114     @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
   115     @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
   116     @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
   117     @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
   118     @{syntax_def string} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\
   119     @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
   120     @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   121     @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*}"} \\[1ex]
   122 
   123     @{text letter} & = & @{text "latin  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
   124     @{text subscript} & = & @{verbatim "\<^sub>"} \\
   125     @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
   126     @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
   127     @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\
   128     @{text sym} & = & @{verbatim "!"}@{text "  |  "}@{verbatim "#"}@{text "  |  "}@{verbatim "$"}@{text "  |  "}@{verbatim "%"}@{text "  |  "}@{verbatim "&"}@{text "  |  "}@{verbatim "*"}@{text "  |  "}@{verbatim "+"}@{text "  |  "}@{verbatim "-"}@{text "  |  "}@{verbatim "/"}@{text "  |"} \\
   129     & & @{verbatim "<"}@{text "  |  "}@{verbatim "="}@{text "  |  "}@{verbatim ">"}@{text "  |  "}@{verbatim "?"}@{text "  |  "}@{verbatim "@"}@{text "  |  "}@{verbatim "^"}@{text "  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "|"}@{text "  |  "}@{verbatim "~"} \\
   130     @{text greek} & = & @{verbatim "\<alpha>"}@{text "  |  "}@{verbatim "\<beta>"}@{text "  |  "}@{verbatim "\<gamma>"}@{text "  |  "}@{verbatim "\<delta>"}@{text "  |"} \\
   131           &   & @{verbatim "\<epsilon>"}@{text "  |  "}@{verbatim "\<zeta>"}@{text "  |  "}@{verbatim "\<eta>"}@{text "  |  "}@{verbatim "\<theta>"}@{text "  |"} \\
   132           &   & @{verbatim "\<iota>"}@{text "  |  "}@{verbatim "\<kappa>"}@{text "  |  "}@{verbatim "\<mu>"}@{text "  |  "}@{verbatim "\<nu>"}@{text "  |"} \\
   133           &   & @{verbatim "\<xi>"}@{text "  |  "}@{verbatim "\<pi>"}@{text "  |  "}@{verbatim "\<rho>"}@{text "  |  "}@{verbatim "\<sigma>"}@{text "  |  "}@{verbatim "\<tau>"}@{text "  |"} \\
   134           &   & @{verbatim "\<upsilon>"}@{text "  |  "}@{verbatim "\<phi>"}@{text "  |  "}@{verbatim "\<chi>"}@{text "  |  "}@{verbatim "\<psi>"}@{text "  |"} \\
   135           &   & @{verbatim "\<omega>"}@{text "  |  "}@{verbatim "\<Gamma>"}@{text "  |  "}@{verbatim "\<Delta>"}@{text "  |  "}@{verbatim "\<Theta>"}@{text "  |"} \\
   136           &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
   137           &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
   138   \end{supertabular}
   139   \end{center}
   140 
   141   A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
   142   which is internally a pair of base name and index (ML type @{ML_type
   143   indexname}).  These components are either separated by a dot as in
   144   @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
   145   "?x1"}.  The latter form is possible if the base name does not end
   146   with digits.  If the index is 0, it may be dropped altogether:
   147   @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
   148   same unknown, with basename @{text "x"} and index 0.
   149 
   150   The syntax of @{syntax_ref string} admits any characters, including
   151   newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}''
   152   (backslash) need to be escaped by a backslash; arbitrary
   153   character codes may be specified as ``@{verbatim \<open>\\<close>}@{text ddd}'',
   154   with three decimal digits.  Alternative strings according to
   155   @{syntax_ref altstring} are analogous, using single back-quotes
   156   instead.
   157 
   158   The body of @{syntax_ref verbatim} may consist of any text not containing
   159   ``@{verbatim "*}"}''; this allows to include quotes without further
   160   escapes, but there is no way to escape ``@{verbatim "*}"}''. Cartouches
   161   do not have this limitation.
   162 
   163   A @{syntax_ref cartouche} consists of arbitrary text, with properly
   164   balanced blocks of ``@{verbatim "\<open>"}~@{text "\<dots>"}~@{verbatim
   165   "\<close>"}''.  Note that the rendering of cartouche delimiters is
   166   usually like this: ``@{text "\<open> \<dots> \<close>"}''.
   167 
   168   Source comments take the form @{verbatim "(*"}~@{text
   169   "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
   170   might prevent this.  Note that this form indicates source comments
   171   only, which are stripped after lexical analysis of the input.  The
   172   Isar syntax also provides proper \emph{document comments} that are
   173   considered as part of the text (see \secref{sec:comments}).
   174 
   175   Common mathematical symbols such as @{text \<forall>} are represented in
   176   Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   177   symbols like this, although proper presentation is left to front-end
   178   tools such as {\LaTeX} or Isabelle/jEdit.  A list of
   179   predefined Isabelle symbols that work well with these tools is given
   180   in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does not belong
   181   to the @{text letter} category, since it is already used differently
   182   in the Pure term language.\<close>
   183 
   184 
   185 section \<open>Common syntax entities\<close>
   186 
   187 text \<open>
   188   We now introduce several basic syntactic entities, such as names,
   189   terms, and theorem specifications, which are factored out of the
   190   actual Isar language elements to be described later.
   191 \<close>
   192 
   193 
   194 subsection \<open>Names\<close>
   195 
   196 text \<open>Entity @{syntax name} usually refers to any name of types,
   197   constants, theorems etc.\ that are to be \emph{declared} or
   198   \emph{defined} (so qualified identifiers are excluded here).  Quoted
   199   strings provide an escape for non-identifier names or those ruled
   200   out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}).
   201   Already existing objects are usually referenced by @{syntax
   202   nameref}.
   203 
   204   @{rail \<open>
   205     @{syntax_def name}: @{syntax ident} | @{syntax symident} |
   206       @{syntax string} | @{syntax nat}
   207     ;
   208     @{syntax_def parname}: '(' @{syntax name} ')'
   209     ;
   210     @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   211   \<close>}
   212 \<close>
   213 
   214 
   215 subsection \<open>Numbers\<close>
   216 
   217 text \<open>The outer lexical syntax (\secref{sec:outer-lex}) admits
   218   natural numbers and floating point numbers.  These are combined as
   219   @{syntax int} and @{syntax real} as follows.
   220 
   221   @{rail \<open>
   222     @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
   223     ;
   224     @{syntax_def real}: @{syntax float} | @{syntax int}
   225   \<close>}
   226 
   227   Note that there is an overlap with the category @{syntax name},
   228   which also includes @{syntax nat}.
   229 \<close>
   230 
   231 
   232 subsection \<open>Comments \label{sec:comments}\<close>
   233 
   234 text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
   235   verbatim}, i.e.\ enclosed in @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"},
   236   or as @{syntax cartouche} @{text "\<open>\<dots>\<close>"}. For convenience, any of the
   237   smaller text units conforming to @{syntax nameref} are admitted as well. A
   238   marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax text}.
   239   Any number of these may occur within Isabelle/Isar commands.
   240 
   241   @{rail \<open>
   242     @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
   243     ;
   244     @{syntax_def comment}: '--' @{syntax text}
   245   \<close>}
   246 \<close>
   247 
   248 
   249 subsection \<open>Type classes, sorts and arities\<close>
   250 
   251 text \<open>
   252   Classes are specified by plain names.  Sorts have a very simple
   253   inner syntax, which is either a single class name @{text c} or a
   254   list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
   255   intersection of these classes.  The syntax of type arities is given
   256   directly at the outer level.
   257 
   258   @{rail \<open>
   259     @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
   260     ;
   261     @{syntax_def sort}: @{syntax nameref}
   262     ;
   263     @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
   264   \<close>}
   265 \<close>
   266 
   267 
   268 subsection \<open>Types and terms \label{sec:types-terms}\<close>
   269 
   270 text \<open>
   271   The actual inner Isabelle syntax, that of types and terms of the
   272   logic, is far too sophisticated in order to be modelled explicitly
   273   at the outer theory level.  Basically, any such entity has to be
   274   quoted to turn it into a single token (the parsing and type-checking
   275   is performed internally later).  For convenience, a slightly more
   276   liberal convention is adopted: quotes may be omitted for any type or
   277   term that is already atomic at the outer level.  For example, one
   278   may just write @{verbatim x} instead of quoted @{verbatim \<open>"x"\<close>}.
   279   Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
   280   "\<forall>"} are available as well, provided these have not been superseded
   281   by commands or other keywords already (such as @{verbatim "="} or
   282   @{verbatim "+"}).
   283 
   284   @{rail \<open>
   285     @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
   286       @{syntax typevar}
   287     ;
   288     @{syntax_def term}: @{syntax nameref} | @{syntax var}
   289     ;
   290     @{syntax_def prop}: @{syntax term}
   291   \<close>}
   292 
   293   Positional instantiations are indicated by giving a sequence of
   294   terms, or the placeholder ``@{text _}'' (underscore), which means to
   295   skip a position.
   296 
   297   @{rail \<open>
   298     @{syntax_def inst}: '_' | @{syntax term}
   299     ;
   300     @{syntax_def insts}: (@{syntax inst} *)
   301   \<close>}
   302 
   303   Type declarations and definitions usually refer to @{syntax
   304   typespec} on the left-hand side.  This models basic type constructor
   305   application at the outer syntax level.  Note that only plain postfix
   306   notation is available here, but no infixes.
   307 
   308   @{rail \<open>
   309     @{syntax_def typespec}:
   310       (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
   311     ;
   312     @{syntax_def typespec_sorts}:
   313       (() | (@{syntax typefree} ('::' @{syntax sort})?) |
   314         '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
   315   \<close>}
   316 \<close>
   317 
   318 
   319 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>
   320 
   321 text \<open>Wherever explicit propositions (or term fragments) occur in a
   322   proof text, casual binding of schematic term variables may be given
   323   specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''.
   324   This works both for @{syntax term} and @{syntax prop}.
   325 
   326   @{rail \<open>
   327     @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
   328     ;
   329     @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
   330   \<close>}
   331 
   332   \medskip Declarations of local variables @{text "x :: \<tau>"} and
   333   logical propositions @{text "a : \<phi>"} represent different views on
   334   the same principle of introducing a local scope.  In practice, one
   335   may usually omit the typing of @{syntax vars} (due to
   336   type-inference), and the naming of propositions (due to implicit
   337   references of current facts).  In any case, Isar proof elements
   338   usually admit to introduce multiple such items simultaneously.
   339 
   340   @{rail \<open>
   341     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
   342     ;
   343     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
   344   \<close>}
   345 
   346   The treatment of multiple declarations corresponds to the
   347   complementary focus of @{syntax vars} versus @{syntax props}.  In
   348   ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}'' the typing refers to all variables, while
   349   in @{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} the naming refers to all propositions
   350   collectively.  Isar language elements that refer to @{syntax vars}
   351   or @{syntax props} typically admit separate typings or namings via
   352   another level of iteration, with explicit @{keyword_ref "and"}
   353   separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   354   \secref{sec:proof-context}.
   355 
   356   @{rail \<open>
   357     @{syntax_def "fixes"}:
   358       ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
   359     ;
   360     @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
   361   \<close>}
   362 
   363   The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
   364   admits specification of mixfix syntax for the entities that are introduced
   365   into the context. An optional suffix ``@{keyword "for"}~@{text "fixes"}''
   366   is admitted in many situations to indicate a so-called ``eigen-context''
   367   of a formal element: the result will be exported and thus generalized over
   368   the given variables.\<close>
   369 
   370 
   371 subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
   372 
   373 text \<open>Attributes have their own ``semi-inner'' syntax, in the sense
   374   that input conforming to @{syntax args} below is parsed by the
   375   attribute a second time.  The attribute argument specifications may
   376   be any sequence of atomic entities (identifiers, strings etc.), or
   377   properly bracketed argument lists.  Below @{syntax atom} refers to
   378   any atomic entity, including any @{syntax keyword} conforming to
   379   @{syntax symident}.
   380 
   381   @{rail \<open>
   382     @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
   383       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
   384       @{syntax keyword} | @{syntax cartouche}
   385     ;
   386     arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
   387     ;
   388     @{syntax_def args}: arg *
   389     ;
   390     @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
   391   \<close>}
   392 
   393   Theorem specifications come in several flavors: @{syntax axmdecl}
   394   and @{syntax thmdecl} usually refer to axioms, assumptions or
   395   results of goal statements, while @{syntax thmdef} collects lists of
   396   existing theorems.  Existing theorems are given by @{syntax thmref}
   397   and @{syntax thmrefs}, the former requires an actual singleton
   398   result.
   399 
   400   There are three forms of theorem references:
   401   \begin{enumerate}
   402   
   403   \item named facts @{text "a"},
   404 
   405   \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
   406 
   407   \item literal fact propositions using token syntax @{syntax_ref altstring}
   408   @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} or @{syntax_ref cartouche}
   409   @{text "\<open>\<phi>\<close>"} (see also method @{method_ref fact}).
   410 
   411   \end{enumerate}
   412 
   413   Any kind of theorem specification may include lists of attributes
   414   both on the left and right hand sides; attributes are applied to any
   415   immediately preceding fact.  If names are omitted, the theorems are
   416   not stored within the theorem database of the theory or proof
   417   context, but any given attributes are applied nonetheless.
   418 
   419   An extra pair of brackets around attributes (like ``@{text
   420   "[[simproc a]]"}'') abbreviates a theorem reference involving an
   421   internal dummy fact, which will be ignored later on.  So only the
   422   effect of the attribute on the background context will persist.
   423   This form of in-place declarations is particularly useful with
   424   commands like @{command "declare"} and @{command "using"}.
   425 
   426   @{rail \<open>
   427     @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
   428     ;
   429     @{syntax_def thmdecl}: thmbind ':'
   430     ;
   431     @{syntax_def thmdef}: thmbind '='
   432     ;
   433     @{syntax_def thmref}:
   434       (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
   435         @{syntax attributes}? |
   436       '[' @{syntax attributes} ']'
   437     ;
   438     @{syntax_def thmrefs}: @{syntax thmref} +
   439     ;
   440 
   441     thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
   442     ;
   443     selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
   444   \<close>}
   445 \<close>
   446 
   447 end