| changeset 8596 | b2ef22670f25 |
| parent 8594 | d2e2a3df6871 |
| child 8828 | 5be2d1745c61 |
--- 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}}