| changeset 8145 | cdd5386eb6fe |
| parent 8102 | 424f6e663977 |
| child 8378 | 73256363a942 |
--- a/doc-src/IsarRef/syntax.tex Wed Jan 26 11:04:38 2000 +0100 +++ b/doc-src/IsarRef/syntax.tex Wed Jan 26 21:10:27 2000 +0100 @@ -101,7 +101,7 @@ \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref} \begin{rail} - name: ident | symident | string + name: ident | symident | string | nat ; parname: '(' name ')' ;