--- 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}