# HG changeset patch
# User wenzelm
# Date 1015599195 -3600
# Node ID 8b2eb3b78cc35fd7f24a1a67eb7392fba76d022d
# Parent  f27cc0a43feb714e432a7598d40a4ffb2ea1f3fe
tuned;

diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/conversion.tex
--- 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:
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/generic.tex
--- 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.
 
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/isar-ref.tex
--- 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}
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/logics.tex
--- 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}
 
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/pure.tex
--- 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$.
   
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/refcard.tex
--- 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}
 
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/syntax.tex
--- 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}
diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/railsetup.sty
--- 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}}}