--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sun Oct 31 13:26:37 2010 +0100
@@ -663,6 +663,7 @@
*}
setup airspeed_velocity_setup
+declare [[airspeed_velocity = 10]]
declare [[airspeed_velocity = 9.9]]
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Oct 31 13:26:37 2010 +0100
@@ -1047,6 +1047,8 @@
\isanewline
\isanewline
\isacommand{declare}\isamarkupfalse%
+\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
\ {\isacharbrackleft}{\isacharbrackleft}airspeed{\isacharunderscore}velocity\ {\isacharequal}\ {\isadigit{9}}{\isachardot}{\isadigit{9}}{\isacharbrackright}{\isacharbrackright}%
\isamarkupsection{Names \label{sec:names}%
}
--- 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}.
*}
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sun Oct 31 11:45:45 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sun Oct 31 13:26:37 2010 +0100
@@ -216,7 +216,6 @@
\railqtok{nameref}.
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
- \indexoutertoken{int}
\begin{rail}
name: ident | symident | string | nat
;
@@ -224,9 +223,29 @@
;
nameref: name | longident
;
+ \end{rail}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Numbers%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The outer lexical syntax (\secref{sec:outer-lex}) admits
+ natural numbers and floating point numbers. These are combined as
+ \hyperlink{syntax.int}{\mbox{\isa{int}}} and \hyperlink{syntax.real}{\mbox{\isa{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 \hyperlink{syntax.nat}{\mbox{\isa{nat}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/Pure/Isar/parse.ML Sun Oct 31 11:45:45 2010 +0100
+++ b/src/Pure/Isar/parse.ML Sun Oct 31 13:26:37 2010 +0100
@@ -195,7 +195,7 @@
val nat = number >> (#1 o Library.read_int o Symbol.explode);
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-val real = float_number >> (the o Real.fromString);
+val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
val tag_name = group "tag name" (short_ident || string);
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);