--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Sun Oct 31 13:26:37 2010 +0100
@@ -197,7 +197,6 @@
\railqtok{nameref}.
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
- \indexoutertoken{int}
\begin{rail}
name: ident | symident | string | nat
;
@@ -205,9 +204,26 @@
;
nameref: name | longident
;
+ \end{rail}
+*}
+
+
+subsection {* Numbers *}
+
+text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
+ natural numbers and floating point numbers. These are combined as
+ @{syntax int} and @{syntax real} as follows.
+
+ \indexoutertoken{int}\indexoutertoken{real}
+ \begin{rail}
int: nat | '-' nat
;
+ real: float | int
+ ;
\end{rail}
+
+ Note that there is an overlap with the category \railqtok{name},
+ which also includes @{syntax nat}.
*}