| changeset 8596 | b2ef22670f25 |
| parent 8594 | d2e2a3df6871 |
| child 8828 | 5be2d1745c61 |
| 8595:06874c5c3cfa | 8596:b2ef22670f25 |
|---|---|
9 |
9 |
10 \makeindex |
10 \makeindex |
11 |
11 |
12 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace} |
12 \railterm{percent,ppercent,underscore,lbrace,rbrace,llbrace,rrbrace} |
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword} |
13 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword} |
14 \railterm{name,nameref,text,type,term,prop,atom} |
|
14 |
15 |
15 \railalias{ident}{\railtoken{ident}} |
16 \railalias{ident}{\railtoken{ident}} |
16 \railalias{longident}{\railtoken{longident}} |
17 \railalias{longident}{\railtoken{longident}} |
17 \railalias{symident}{\railtoken{symident}} |
18 \railalias{symident}{\railtoken{symident}} |
18 \railalias{var}{\railtoken{var}} |
19 \railalias{var}{\railtoken{var}} |