1.1 --- a/doc-src/IsarRef/generic.tex	Mon Mar 27 18:09:49 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Mar 27 18:10:11 2000 +0200
     1.3 @@ -365,16 +365,16 @@
     1.4  
     1.5  \begin{descr}
     1.6  \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
     1.7 -  according to the arguments given.  Note that the \railtoken{only} modifier
     1.8 +  according to the arguments given.  Note that the \railtterm{only} modifier
     1.9    first removes all other rewrite rules, congruences, and looper tactics
    1.10 -  (including splits), and then behaves like \railtoken{add}.
    1.11 +  (including splits), and then behaves like \railtterm{add}.
    1.12    
    1.13 -  The \railtoken{split} modifiers add or delete rules for the Splitter (see
    1.14 +  The \railtterm{split} modifiers add or delete rules for the Splitter (see
    1.15    also \cite{isabelle-ref}), the default is to add.  This works only if the
    1.16    Simplifier method has been properly setup to include the Splitter (all major
    1.17    object logics such HOL, HOLCF, FOL, ZF do this already).
    1.18    
    1.19 -  The \railtoken{other} modifier ignores its arguments.  Nevertheless,
    1.20 +  The \railtterm{other} modifier ignores its arguments.  Nevertheless,
    1.21    additional kinds of rules may be declared by including appropriate
    1.22    attributes in the specification.
    1.23  \item [$simp_all$] is similar to $simp$, but acts on all goals.
    1.24 @@ -536,7 +536,7 @@
    1.25    \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
    1.26    modifier arguments correspond to those given in \S\ref{sec:simp} and
    1.27    \S\ref{sec:classical-auto}.  Just note that the ones related to the
    1.28 -  Simplifier are prefixed by \railtoken{simp} here.
    1.29 +  Simplifier are prefixed by \railtterm{simp} here.
    1.30    
    1.31    Facts provided by forward chaining are inserted into the goal before doing
    1.32    the search.  The ``!''~argument causes the full context of assumptions to be

     2.1 --- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:09:49 2000 +0200
     2.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:10:11 2000 +0200
     2.3 @@ -12,6 +12,18 @@
     2.4  \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
     2.5  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
     2.6  
     2.7 +\railalias{ident}{\railtoken{ident}}
     2.8 +\railalias{longident}{\railtoken{longident}}
     2.9 +\railalias{symident}{\railtoken{symident}}
    2.10 +\railalias{var}{\railtoken{var}}
    2.11 +\railalias{textvar}{\railtoken{textvar}}
    2.12 +\railalias{typefree}{\railtoken{typefree}}
    2.13 +\railalias{typevar}{\railtoken{typevar}}
    2.14 +\railalias{nat}{\railtoken{nat}}
    2.15 +\railalias{string}{\railtoken{string}}
    2.16 +\railalias{verbatim}{\railtoken{verbatim}}
    2.17 +\railalias{keyword}{\railtoken{keyword}}
    2.18 +
    2.19  \railalias{name}{\railqtoken{name}}
    2.20  \railalias{nameref}{\railqtoken{nameref}}
    2.21  \railalias{text}{\railqtoken{text}}