doc-src/IsarRef/Thy/Outer_Syntax.thy

   out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
   Already existing objects are usually referenced by
   \railqtok{nameref}.
 
   \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
-  \indexoutertoken{int}
   \begin{rail}
     name: ident | symident | string | nat
     ;
     parname: '(' name ')'
     ;
     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
     ;
-  \end{rail}
+    real: float | int
+    ;
+  \end{rail}
+
+  Note that there is an overlap with the category \railqtok{name},
+  which also includes @{syntax nat}.
 *}
 
 
 subsection {* Comments \label{sec:comments} *}