1.1 --- a/doc-src/IsarRef/isar-ref.tex Fri Mar 08 15:33:32 2002 +0100
1.2 +++ b/doc-src/IsarRef/isar-ref.tex Fri Mar 08 15:53:15 2002 +0100
1.3 @@ -24,25 +24,25 @@
1.4 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
1.5 \railterm{name,nameref,text,type,term,prop,atom}
1.6
1.7 -\railalias{ident}{\railtoken{ident}}
1.8 -\railalias{longident}{\railtoken{longident}}
1.9 -\railalias{symident}{\railtoken{symident}}
1.10 -\railalias{var}{\railtoken{var}}
1.11 -\railalias{textvar}{\railtoken{textvar}}
1.12 -\railalias{typefree}{\railtoken{typefree}}
1.13 -\railalias{typevar}{\railtoken{typevar}}
1.14 -\railalias{nat}{\railtoken{nat}}
1.15 -\railalias{string}{\railtoken{string}}
1.16 -\railalias{verbatim}{\railtoken{verbatim}}
1.17 -\railalias{keyword}{\railtoken{keyword}}
1.18 +\railalias{ident}{\railtok{ident}}
1.19 +\railalias{longident}{\railtok{longident}}
1.20 +\railalias{symident}{\railtok{symident}}
1.21 +\railalias{var}{\railtok{var}}
1.22 +\railalias{textvar}{\railtok{textvar}}
1.23 +\railalias{typefree}{\railtok{typefree}}
1.24 +\railalias{typevar}{\railtok{typevar}}
1.25 +\railalias{nat}{\railtok{nat}}
1.26 +\railalias{string}{\railtok{string}}
1.27 +\railalias{verbatim}{\railtok{verbatim}}
1.28 +\railalias{keyword}{\railtok{keyword}}
1.29
1.30 -\railalias{name}{\railqtoken{name}}
1.31 -\railalias{nameref}{\railqtoken{nameref}}
1.32 -\railalias{text}{\railqtoken{text}}
1.33 -\railalias{type}{\railqtoken{type}}
1.34 -\railalias{term}{\railqtoken{term}}
1.35 -\railalias{prop}{\railqtoken{prop}}
1.36 -\railalias{atom}{\railqtoken{atom}}
1.37 +\railalias{name}{\railqtok{name}}
1.38 +\railalias{nameref}{\railqtok{nameref}}
1.39 +\railalias{text}{\railqtok{text}}
1.40 +\railalias{type}{\railqtok{type}}
1.41 +\railalias{term}{\railqtok{term}}
1.42 +\railalias{prop}{\railqtok{prop}}
1.43 +\railalias{atom}{\railqtok{atom}}
1.44
1.45 \newcommand{\drv}{\mathrel{\vdash}}
1.46 \newcommand{\edrv}{\mathop{\drv}\nolimits}