doc-src/IsarRef/Thy/Outer_Syntax.thy
changeset 40291 012ed4426fda
parent 40290 47f572aff50a
child 40296 ac4d75f86d97
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Oct 30 16:33:58 2010 +0200
@@ -366,7 +366,7 @@
 
   \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   \begin{rail}
-    atom: nameref | typefree | typevar | var | nat | keyword
+    atom: nameref | typefree | typevar | var | nat | float | keyword
     ;
     arg: atom | '(' args ')' | '[' args ']'
     ;