# HG changeset patch
# User wenzelm
# Date 954173411 -7200
# Node ID d2e2a3df6871c6e8040b2e62306854b7e49c5538
# Parent  68619606c5d1a1f926b816454228ca77e622e875
rail token vs. terminal;

diff -r 68619606c5d1 -r d2e2a3df6871 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Mar 27 18:09:49 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Mar 27 18:10:11 2000 +0200
@@ -365,16 +365,16 @@
 
 \begin{descr}
 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
-  according to the arguments given.  Note that the \railtoken{only} modifier
+  according to the arguments given.  Note that the \railtterm{only} modifier
   first removes all other rewrite rules, congruences, and looper tactics
-  (including splits), and then behaves like \railtoken{add}.
+  (including splits), and then behaves like \railtterm{add}.
   
-  The \railtoken{split} modifiers add or delete rules for the Splitter (see
+  The \railtterm{split} modifiers add or delete rules for the Splitter (see
   also \cite{isabelle-ref}), the default is to add.  This works only if the
   Simplifier method has been properly setup to include the Splitter (all major
   object logics such HOL, HOLCF, FOL, ZF do this already).
   
-  The \railtoken{other} modifier ignores its arguments.  Nevertheless,
+  The \railtterm{other} modifier ignores its arguments.  Nevertheless,
   additional kinds of rules may be declared by including appropriate
   attributes in the specification.
 \item [$simp_all$] is similar to $simp$, but acts on all goals.
@@ -536,7 +536,7 @@
   \texttt{auto_tac} in \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 \railtoken{simp} here.
+  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
diff -r 68619606c5d1 -r d2e2a3df6871 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:09:49 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:10:11 2000 +0200
@@ -12,6 +12,18 @@
 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
 
+\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{name}{\railqtoken{name}}
 \railalias{nameref}{\railqtoken{nameref}}
 \railalias{text}{\railqtoken{text}}