--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Fri Oct 29 23:15:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Oct 30 15:26:40 2010 +0200
@@ -108,6 +108,7 @@
@{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
@{syntax_def symident} & = & @{text "sym\<^sup>+ | "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
@{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
+ @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
@{syntax_def var} & = & @{verbatim "?"}@{text "ident | "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
@{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
@{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree | "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\