# HG changeset patch
# User wenzelm
# Date 1230058161 -3600
# Node ID 461f34ed79ec8b88a09c5d9bf691979e865ca1fb
# Parent  89f76a58a378dbf1efae582626b1aa60ca4596e7
added float_token, and num_const, float_const;
tuned;

diff -r 89f76a58a378 -r 461f34ed79ec doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Dec 23 19:27:42 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Dec 23 19:49:21 2008 +0100
@@ -683,17 +683,23 @@
     @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
     @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
     @{syntax_def (inner) num} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
+    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
 
     @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
   \end{supertabular}
   \end{center}
 
-  The token categories @{syntax_ref (inner) num}, @{syntax_ref (inner)
-  xnum}, and @{syntax_ref (inner) xstr} are not used in Pure.
-  Object-logics may implement numerals and string constants by adding
-  appropriate syntax declarations, together with some translation
-  functions (e.g.\ see Isabelle/HOL).
+  The token categories @{syntax (inner) num}, @{syntax (inner)
+  float_token}, @{syntax (inner) xnum}, and @{syntax (inner) xstr} are
+  not used in Pure.  Object-logics may implement numerals and string
+  constants by adding appropriate syntax declarations, together with
+  some translation functions (e.g.\ see Isabelle/HOL).
+
+  The derived categories @{syntax_def (inner) num_const} and
+  @{syntax_def (inner) float_const} provide robust access to @{syntax
+  (inner) num}, and @{syntax (inner) float_token}, respectively: the
+  syntax tree holds a syntactic constant instead of a free variable.
 *}