--- 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}}