# HG changeset patch
# User wenzelm
# Date 954184403 -7200
# Node ID b2ef22670f25f39eaadb870c560103e46b6cfa28
# Parent  06874c5c3cfa5abaeaa019ae3f374f2cf26f85f0
tuned;

diff -r 06874c5c3cfa -r b2ef22670f25 doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 21:13:06 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon Mar 27 21:13:23 2000 +0200
@@ -11,6 +11,7 @@
 
 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace}
 \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}}