diff -r b80ea2b32f8e -r 574ab125a03b doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Aug 17 10:32:20 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Thu Aug 17 10:32:44 2000 +0200
@@ -47,6 +47,9 @@
 should not be confused, though.
 
 %FIXME keyword, command
+\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
+\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
+\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
 \begin{matharray}{rcl}
   ident & = & letter~quasiletter^* \\
   longident & = & ident\verb,.,ident~\dots~ident \\
@@ -107,6 +110,7 @@
 \railqtoken{nameref}.
 
 \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
+\indexoutertoken{int}
 \begin{rail}
   name: ident | symident | string | nat
   ;
@@ -114,6 +118,8 @@
   ;
   nameref: name | longident
   ;
+  int: nat | '-' nat
+  ;
 \end{rail}