1.1 --- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:09:49 2000 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 18:10:11 2000 +0200
     1.3 @@ -12,6 +12,18 @@
     1.4  \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
     1.5  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
     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 +
    1.19  \railalias{name}{\railqtoken{name}}
    1.20  \railalias{nameref}{\railqtoken{nameref}}
    1.21  \railalias{text}{\railqtoken{text}}