--- a/doc-src/IsarRef/conversion.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/conversion.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
+\chapter{Isabelle/Isar conversion guide}\label{ap:conv}
Subsequently, we give a few practical hints on working in a mixed environment
of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
@@ -39,21 +39,21 @@
\begin{descr}
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
in the current theory context, including any ancestor node.
-
+
The convention of old-style theories was to bind any theorem as an ML value
as well. New-style theories no longer do this, so ML code may require
\texttt{thm~"foo"} rather than just \texttt{foo}.
-
+
\item [$\mathtt{the_context()}$] refers to the current theory context.
-
+
Old-style theories often use the ML binding \texttt{thy}, which is
dynamically created by the ML code generated from old theory source. This
is no longer the recommended way in any case! Function \texttt{the_context}
should be used for old scripts as well.
-
+
\item [$\mathtt{theory}~name$] retrieves the named theory from the global
theory-loader database.
-
+
The ML code generated from old-style theories would include an ML binding
$name\mathtt{.thy}$ as part of an ML structure.
\end{descr}
@@ -72,11 +72,11 @@
these later.
\begin{descr}
-
+
\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
ML. This already manages entry in the theorem database of the current
theory context.
-
+
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
store theorems that have been produced in ML in an ad-hoc manner.
@@ -133,13 +133,13 @@
\item Quoted strings may contain arbitrary white space, and span several lines
without requiring \verb,\,\,\dots\verb,\, escapes.
\item Names may always be quoted.
-
+
The old syntax would occasionally demand plain identifiers vs.\ quoted
strings to accommodate certain syntactic features.
\item Types and terms have to be \emph{atomic} as far as the theory syntax is
concerned; this typically requires quoting of input strings, e.g.\ ``$x +
y$''.
-
+
The old theory syntax used to fake part of the syntax of types in order to
require less quoting in common cases; this was hard to predict, though. On
the other hand, Isar does not require quotes for simple terms, such as plain
@@ -300,12 +300,12 @@
rule applications (based on higher-order resolution). The space of resolution
tactics has the following main dimensions.
\begin{enumerate}
-\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
+\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
\texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
\texttt{forward_tac}).
-\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
+\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
\texttt{res_inst_tac}).
-\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
+\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
\texttt{rtac}).
\end{enumerate}
@@ -348,9 +348,9 @@
The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
-methods (see \S\ref{sec:simp}). Note that there is no individual goal
-addressing available, simplification acts either on the first goal ($simp$)
-or all goals ($simp_all$).
+methods (see \S\ref{sec:simplifier}). Note that there is no individual goal
+addressing available, simplification acts either on the first goal ($simp$) or
+all goals ($simp_all$).
\begin{matharray}{lll}
\texttt{Asm_full_simp_tac 1} & & simp \\
@@ -361,8 +361,9 @@
\end{matharray}
Isar also provides separate method modifier syntax for augmenting the
-Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
-in ML. A typical ML expression with simpset changes looks like this:
+Simplifier context (see \S\ref{sec:simplifier}), which is known as the
+``simpset'' in ML. A typical ML expression with simpset changes looks like
+this:
\begin{ttbox}
asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
\end{ttbox}
@@ -380,7 +381,7 @@
automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar
methods usually share the same base name, such as $blast$, $fast$, $clarify$
-etc.\ (see \S\ref{sec:classical-auto}).
+etc.\ (see \S\ref{sec:classical}).
Similar to the Simplifier, there is separate method modifier syntax for
augmenting the Classical Reasoner context, which is known as the ``claset'' in
@@ -442,14 +443,13 @@
\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
are not available in Isar, since there is no direct goal addressing.
Nevertheless, some basic methods address all goals internally, notably
-$simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be
-often replaced by ``$+$'' (repeat at least once), although this usually has a
-different operational behavior, such as solving goals in a different order.
+$simp_all$ (see \S\ref{sec:simplifier}). Also note that \texttt{ALLGOALS} may
+be often replaced by ``$+$'' (repeat at least once), although this usually has
+a different operational behavior, such as solving goals in a different order.
\medskip Iterated resolution, such as
\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
-using the $intro$ and $elim$ methods of Isar (see
-\S\ref{sec:classical-basic}).
+using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
@@ -559,8 +559,7 @@
machine-checked formal proof. Depending on the context of application, this
might be even indispensable to start with!
-
-%%% Local Variables:
+%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
-%%% End:
+%%% End:
--- a/doc-src/IsarRef/generic.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/generic.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Generic Tools and Packages}\label{ch:gen-tools}
+\chapter{Generic tools and packages}\label{ch:gen-tools}
\section{Theory specification commands}
@@ -62,6 +62,7 @@
that are modeled after the Isar proof context commands (cf.\
\S\ref{sec:proof-context}).
+
\subsubsection{Localized commands}
Existing locales may be augmented later on by adding new facts. Note that the
@@ -238,10 +239,9 @@
\end{matharray}
Typically, the soundness proof is relatively straight-forward, often just by
-canonical automated tools such as ``$\BY{simp}$'' (see \S\ref{sec:simp}) or
-``$\BY{blast}$'' (see \S\ref{sec:classical-auto}). Accordingly, the
-``$that$'' reduction above is declared as simplification and introduction
-rule.
+canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
+Accordingly, the ``$that$'' reduction above is declared as simplification and
+introduction rule.
\medskip
@@ -466,9 +466,9 @@
\item [$elim_format$] turns a destruction rule into elimination rule format,
by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
B$.
-
- Note that the Classical Reasoner (\S\ref{sec:classical-att}) provides its
- own version of this operation.
+
+ Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
+ version of this operation.
\item [$standard$] puts a theorem into the standard form of object-rules at
the outermost theory level. Note that this operation violates the local
@@ -612,7 +612,7 @@
\subsection{The Simplifier}\label{sec:simplifier}
-\subsubsection{Simplification methods}\label{sec:simp}
+\subsubsection{Simplification methods}
\indexisarmeth{simp}\indexisarmeth{simp-all}
\begin{matharray}{rcl}
@@ -737,13 +737,12 @@
\end{rail}
\begin{descr}
-
+
\item [$simplified~\vec a$] causes a theorem to be simplified, either by
exactly the specified rules $\vec a$, or the implicit Simplifier context if
no arguments are given. The result is fully simplified by default,
including assumptions and conclusion; the options $no_asm$ etc.\ tune the
- Simplifier in the same way as the for the $simp$ method (see
- \S\ref{sec:simp}).
+ Simplifier in the same way as the for the $simp$ method.
Note that forward simplification restricts the simplifier to its most basic
operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
@@ -753,7 +752,7 @@
\end{descr}
-\subsubsection{Low-level equational reasoning}\label{sec:basic-eq}
+\subsubsection{Low-level equational reasoning}
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
\begin{matharray}{rcl}
@@ -787,15 +786,15 @@
\item [$split~\vec a$] performs single-step case splitting using rules $thms$.
By default, splitting is performed in the conclusion of a goal; the $asm$
option indicates to operate on assumptions instead.
-
+
Note that the $simp$ method already involves repeated application of split
- rules as declared in the current context (see \S\ref{sec:simp}).
+ rules as declared in the current context.
\end{descr}
\subsection{The Classical Reasoner}\label{sec:classical}
-\subsubsection{Basic methods}\label{sec:classical-basic}
+\subsubsection{Basic methods}
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
\indexisarmeth{intro}\indexisarmeth{elim}
@@ -835,7 +834,7 @@
\end{descr}
-\subsubsection{Automated methods}\label{sec:classical-auto}
+\subsubsection{Automated methods}
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
@@ -908,9 +907,9 @@
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac},
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The
- modifier arguments correspond to those given in \S\ref{sec:simp} and
- \S\ref{sec:classical-auto}. Just note that the ones related to the
- Simplifier are prefixed by \railtterm{simp} here.
+ modifier arguments correspond to those given in \S\ref{sec:simplifier} and
+ \S\ref{sec:classical}. Just note that the ones related to the Simplifier
+ are prefixed by \railtterm{simp} here.
Facts provided by forward chaining are inserted into the goal before doing
the search. The ``!''~argument causes the full context of assumptions to be
@@ -918,7 +917,7 @@
\end{descr}
-\subsubsection{Declaring rules}\label{sec:classical-mod}
+\subsubsection{Declaring rules}
\indexisarcmd{print-claset}
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
@@ -969,7 +968,7 @@
\end{descr}
-\subsubsection{Classical operations}\label{sec:classical-att}
+\subsubsection{Classical operations}
\indexisaratt{elim-format}\indexisaratt{swapped}
@@ -994,7 +993,7 @@
\subsection{Proof by cases and induction}\label{sec:cases-induct}
-\subsubsection{Rule contexts}\label{sec:rule-cases}
+\subsubsection{Rule contexts}
\indexisarcmd{case}\indexisarcmd{print-cases}
\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
@@ -1106,9 +1105,9 @@
and induction over datatypes, inductive sets, and recursive functions. The
corresponding rules may be specified and instantiated in a casual manner.
Furthermore, these methods provide named local contexts that may be invoked
-via the $\CASENAME$ proof command within the subsequent proof text (cf.\
-\S\ref{sec:rule-cases}). This accommodates compact proof texts even when
-reasoning about large specifications.
+via the $\CASENAME$ proof command within the subsequent proof text. This
+accommodates compact proof texts even when reasoning about large
+specifications.
\begin{rail}
'cases' spec
@@ -1175,16 +1174,16 @@
\end{descr}
-Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
-determined by the instantiated rule as specified in the text. Beyond that,
-the $induct$ method guesses further instantiations from the goal specification
-itself. Any persisting unresolved schematic variables of the resulting rule
-will render the the corresponding case invalid. The term binding
-$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each
-case, provided that term is fully specified.
+Above methods produce named local contexts, as determined by the instantiated
+rule as specified in the text. Beyond that, the $induct$ method guesses
+further instantiations from the goal specification itself. Any persisting
+unresolved schematic variables of the resulting rule will render the the
+corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case}
+for the conclusion will be provided with each case, provided that term is
+fully specified.
-The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all
-named cases present in the current proof state.
+The $\isarkeyword{print_cases}$ command prints all named cases present in the
+current proof state.
\medskip
@@ -1242,10 +1241,10 @@
corresponding methods of the same name. Certain definitional packages of
object-logics usually declare emerging cases and induction rules as
expected, so users rarely need to intervene.
-
+
Manual rule declarations usually include the the $case_names$ and $ps$
attributes to adjust names of cases and parameters of a rule (see
- \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
+ \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
for ``set'' rules.
--- a/doc-src/IsarRef/isar-ref.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Fri Mar 08 15:53:15 2002 +0100
@@ -24,25 +24,25 @@
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
\railterm{name,nameref,text,type,term,prop,atom}
-\railalias{ident}{\railtoken{ident}}
-\railalias{longident}{\railtoken{longident}}
-\railalias{symident}{\railtoken{symident}}
-\railalias{var}{\railtoken{var}}
-\railalias{textvar}{\railtoken{textvar}}
-\railalias{typefree}{\railtoken{typefree}}
-\railalias{typevar}{\railtoken{typevar}}
-\railalias{nat}{\railtoken{nat}}
-\railalias{string}{\railtoken{string}}
-\railalias{verbatim}{\railtoken{verbatim}}
-\railalias{keyword}{\railtoken{keyword}}
+\railalias{ident}{\railtok{ident}}
+\railalias{longident}{\railtok{longident}}
+\railalias{symident}{\railtok{symident}}
+\railalias{var}{\railtok{var}}
+\railalias{textvar}{\railtok{textvar}}
+\railalias{typefree}{\railtok{typefree}}
+\railalias{typevar}{\railtok{typevar}}
+\railalias{nat}{\railtok{nat}}
+\railalias{string}{\railtok{string}}
+\railalias{verbatim}{\railtok{verbatim}}
+\railalias{keyword}{\railtok{keyword}}
-\railalias{name}{\railqtoken{name}}
-\railalias{nameref}{\railqtoken{nameref}}
-\railalias{text}{\railqtoken{text}}
-\railalias{type}{\railqtoken{type}}
-\railalias{term}{\railqtoken{term}}
-\railalias{prop}{\railqtoken{prop}}
-\railalias{atom}{\railqtoken{atom}}
+\railalias{name}{\railqtok{name}}
+\railalias{nameref}{\railqtok{nameref}}
+\railalias{text}{\railqtok{text}}
+\railalias{type}{\railqtok{type}}
+\railalias{term}{\railqtok{term}}
+\railalias{prop}{\railqtok{prop}}
+\railalias{atom}{\railqtok{atom}}
\newcommand{\drv}{\mathrel{\vdash}}
\newcommand{\edrv}{\mathop{\drv}\nolimits}
--- a/doc-src/IsarRef/logics.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/logics.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Object-logic Specific Elements}\label{ch:logics}
+\chapter{Object-logic specific elements}\label{ch:logics}
\section{General logic setup}\label{sec:object-logic}
--- a/doc-src/IsarRef/pure.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Basic Language Elements}\label{ch:pure-syntax}
+\chapter{Basic language elements}\label{ch:pure-syntax}
Subsequently, we introduce the main part of Pure theory and proof commands,
together with fundamental proof methods and attributes.
@@ -508,8 +508,8 @@
Syntax translation functions written in ML admit almost arbitrary
manipulations of Isabelle's inner syntax. Any of the above commands have a
-single \railqtoken{text} argument that refers to an ML expression of
-appropriate type.
+single \railqtok{text} argument that refers to an ML expression of appropriate
+type.
\begin{ttbox}
val parse_ast_translation : (string * (ast list -> ast)) list
@@ -837,8 +837,7 @@
Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
be bound automatically, see also \S\ref{sec:term-abbrev}. Furthermore, the
local context of a (non-atomic) goal is provided via the
-$rule_context$\indexisarcase{rule-context} case, see also
-\S\ref{sec:rule-cases}.
+$rule_context$\indexisarcase{rule-context} case.
\medskip
@@ -1042,7 +1041,7 @@
the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
most aggressively.
- The classical reasoner (see \S\ref{sec:classical-basic}) introduces its own
+ The classical reasoner (see \S\ref{sec:classical}) introduces its own
variants of these attributes; use qualified names to access the present
versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
--- a/doc-src/IsarRef/refcard.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/refcard.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Isabelle/Isar Quick Reference}\label{ap:refcard}
+\chapter{Isabelle/Isar quick reference}\label{ap:refcard}
\section{Proof commands}
--- a/doc-src/IsarRef/syntax.tex Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/IsarRef/syntax.tex Fri Mar 08 15:53:15 2002 +0100
@@ -1,5 +1,5 @@
-\chapter{Syntax Primitives}
+\chapter{Syntax primitives}
The rather generic framework of Isabelle/Isar syntax emerges from three main
syntactic categories: \emph{commands} of the top-level Isar engine (covering
@@ -130,21 +130,21 @@
Isar language elements to be described later.
Note that some of the basic syntactic entities introduced below (e.g.\
-\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\
+\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\
\railnonterm{sort}), especially for the sake of error messages. E.g.\ syntax
-elements like $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
-would really report a missing name or type rather than any of the constituent
-primitive tokens such as \railtoken{ident} or \railtoken{string}.
+elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would
+really report a missing name or type rather than any of the constituent
+primitive tokens such as \railtok{ident} or \railtok{string}.
\subsection{Names}
-Entity \railqtoken{name} usually refers to any name of types, constants,
+Entity \railqtok{name} usually refers to any name of types, constants,
theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
identifiers are excluded here). Quoted strings provide an escape for
non-identifier names or those ruled out by outer syntax keywords (e.g.\
\verb|"let"|). Already existing objects are usually referenced by
-\railqtoken{nameref}.
+\railqtok{nameref}.
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
\indexoutertoken{int}
@@ -162,12 +162,11 @@
\subsection{Comments}\label{sec:comments}
-Large chunks of plain \railqtoken{text} are usually given
-\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For
-convenience, any of the smaller text units conforming to \railqtoken{nameref}
-are admitted as well. A marginal \railnonterm{comment} is of the form
-\texttt{--} \railqtoken{text}. Any number of these may occur within
-Isabelle/Isar commands.
+Large chunks of plain \railqtok{text} are usually given \railtok{verbatim},
+i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For convenience, any of the
+smaller text units conforming to \railqtok{nameref} are admitted as well. A
+marginal \railnonterm{comment} is of the form \texttt{--} \railqtok{text}.
+Any number of these may occur within Isabelle/Isar commands.
\indexoutertoken{text}\indexouternonterm{comment}
\begin{rail}
@@ -269,7 +268,7 @@
;
\end{rail}
-Here the \railtoken{string} specifications refer to the actual mixfix template
+Here the \railtok{string} specifications refer to the actual mixfix template
(see also \cite{isabelle-ref}), which may include literal text, spacing,
blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
(printed as ``\i'') represents an index argument that specifies an implicit
@@ -287,7 +286,7 @@
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once). In practice,
proof methods are usually just a comma separated list of
-\railqtoken{nameref}~\railnonterm{args} specifications. Note that parentheses
+\railqtok{nameref}~\railnonterm{args} specifications. Note that parentheses
may be dropped for single method specifications (with no arguments).
\indexouternonterm{method}
@@ -317,8 +316,8 @@
\railnonterm{args} below is parsed by the attribute a second time. The
attribute argument specifications may be any sequence of atomic entities
(identifiers, strings etc.), or properly bracketed argument lists. Below
-\railqtoken{atom} refers to any atomic entity, including any
-\railtoken{keyword} conforming to \railtoken{symident}.
+\railqtok{atom} refers to any atomic entity, including any \railtok{keyword}
+conforming to \railtok{symident}.
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
\begin{rail}
@@ -366,8 +365,8 @@
Wherever explicit propositions (or term fragments) occur in a proof text,
casual binding of schematic term variables may be given specified via patterns
of the form ``$\ISS{p@1\;\dots}{p@n}$''. There are separate versions
-available for \railqtoken{term}s and \railqtoken{prop}s. The latter provides
-a $\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
+available for \railqtok{term}s and \railqtok{prop}s. The latter provides a
+$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
\indexouternonterm{termpat}\indexouternonterm{proppat}
\begin{rail}
--- a/doc-src/railsetup.sty Fri Mar 08 15:33:32 2002 +0100
+++ b/doc-src/railsetup.sty Fri Mar 08 15:53:15 2002 +0100
@@ -27,6 +27,6 @@
\def\rail@namefont{\small\rmfamily\itshape}
\def\rail@indexfont{\small\rmfamily\itshape}
\newcommand{\railtterm}[1]{{\texttt{#1}}}
-\newcommand{\railtoken}[1]{{\textrm{#1}}}
-\newcommand{\railqtoken}[1]{{\rmfamily\textsl{#1}}}
+\newcommand{\railtok}[1]{{\textrm{#1}}}
+\newcommand{\railqtok}[1]{{\rmfamily\textsl{#1}}}
\newcommand{\railnonterm}[1]{{\emph{#1}}}