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