diff -r d4923a7f42c1 -r ac4d75f86d97 doc-src/IsarRef/Thy/Outer_Syntax.thy
--- 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}.
 *}