doc-src/IsarRef/syntax.tex
changeset 13048 8b2eb3b78cc3
parent 13039 cfcc1f6f21df
child 13827 c690cb885db4
     1.1 --- a/doc-src/IsarRef/syntax.tex	Thu Mar 07 19:04:00 2002 +0100
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Fri Mar 08 15:53:15 2002 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  
     1.5 -\chapter{Syntax Primitives}
     1.6 +\chapter{Syntax primitives}
     1.7  
     1.8  The rather generic framework of Isabelle/Isar syntax emerges from three main
     1.9  syntactic categories: \emph{commands} of the top-level Isar engine (covering
    1.10 @@ -130,21 +130,21 @@
    1.11  Isar language elements to be described later.
    1.12  
    1.13  Note that some of the basic syntactic entities introduced below (e.g.\ 
    1.14 -\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\ 
    1.15 +\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\ 
    1.16  \railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
    1.17 -elements like $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
    1.18 -would really report a missing name or type rather than any of the constituent
    1.19 -primitive tokens such as \railtoken{ident} or \railtoken{string}.
    1.20 +elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would
    1.21 +really report a missing name or type rather than any of the constituent
    1.22 +primitive tokens such as \railtok{ident} or \railtok{string}.
    1.23  
    1.24  
    1.25  \subsection{Names}
    1.26  
    1.27 -Entity \railqtoken{name} usually refers to any name of types, constants,
    1.28 +Entity \railqtok{name} usually refers to any name of types, constants,
    1.29  theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
    1.30  identifiers are excluded here).  Quoted strings provide an escape for
    1.31  non-identifier names or those ruled out by outer syntax keywords (e.g.\ 
    1.32  \verb|"let"|).  Already existing objects are usually referenced by
    1.33 -\railqtoken{nameref}.
    1.34 +\railqtok{nameref}.
    1.35  
    1.36  \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
    1.37  \indexoutertoken{int}
    1.38 @@ -162,12 +162,11 @@
    1.39  
    1.40  \subsection{Comments}\label{sec:comments}
    1.41  
    1.42 -Large chunks of plain \railqtoken{text} are usually given
    1.43 -\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For
    1.44 -convenience, any of the smaller text units conforming to \railqtoken{nameref}
    1.45 -are admitted as well.  A marginal \railnonterm{comment} is of the form
    1.46 -\texttt{--} \railqtoken{text}.  Any number of these may occur within
    1.47 -Isabelle/Isar commands.
    1.48 +Large chunks of plain \railqtok{text} are usually given \railtok{verbatim},
    1.49 +i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For convenience, any of the
    1.50 +smaller text units conforming to \railqtok{nameref} are admitted as well.  A
    1.51 +marginal \railnonterm{comment} is of the form \texttt{--} \railqtok{text}.
    1.52 +Any number of these may occur within Isabelle/Isar commands.
    1.53  
    1.54  \indexoutertoken{text}\indexouternonterm{comment}
    1.55  \begin{rail}
    1.56 @@ -269,7 +268,7 @@
    1.57    ;
    1.58  \end{rail}
    1.59  
    1.60 -Here the \railtoken{string} specifications refer to the actual mixfix template
    1.61 +Here the \railtok{string} specifications refer to the actual mixfix template
    1.62  (see also \cite{isabelle-ref}), which may include literal text, spacing,
    1.63  blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
    1.64  (printed as ``\i'') represents an index argument that specifies an implicit
    1.65 @@ -287,7 +286,7 @@
    1.66  ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
    1.67  ``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
    1.68  proof methods are usually just a comma separated list of
    1.69 -\railqtoken{nameref}~\railnonterm{args} specifications.  Note that parentheses
    1.70 +\railqtok{nameref}~\railnonterm{args} specifications.  Note that parentheses
    1.71  may be dropped for single method specifications (with no arguments).
    1.72  
    1.73  \indexouternonterm{method}
    1.74 @@ -317,8 +316,8 @@
    1.75  \railnonterm{args} below is parsed by the attribute a second time.  The
    1.76  attribute argument specifications may be any sequence of atomic entities
    1.77  (identifiers, strings etc.), or properly bracketed argument lists.  Below
    1.78 -\railqtoken{atom} refers to any atomic entity, including any
    1.79 -\railtoken{keyword} conforming to \railtoken{symident}.
    1.80 +\railqtok{atom} refers to any atomic entity, including any \railtok{keyword}
    1.81 +conforming to \railtok{symident}.
    1.82  
    1.83  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
    1.84  \begin{rail}
    1.85 @@ -366,8 +365,8 @@
    1.86  Wherever explicit propositions (or term fragments) occur in a proof text,
    1.87  casual binding of schematic term variables may be given specified via patterns
    1.88  of the form ``$\ISS{p@1\;\dots}{p@n}$''.  There are separate versions
    1.89 -available for \railqtoken{term}s and \railqtoken{prop}s.  The latter provides
    1.90 -a $\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    1.91 +available for \railqtok{term}s and \railqtok{prop}s.  The latter provides a
    1.92 +$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
    1.93  
    1.94  \indexouternonterm{termpat}\indexouternonterm{proppat}
    1.95  \begin{rail}