1.1 --- a/doc-src/TutorialI/Types/numerics.tex Thu Nov 19 10:49:43 2009 +0100
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex Thu Nov 19 10:58:36 2009 +0000
1.3 @@ -347,8 +347,7 @@
1.4 \ 1.\ P\ (2\ /\ 5)
1.5 \end{isabelle}
1.6 Exponentiation can express floating-point values such as
1.7 -\isa{2 * 10\isacharcircum6}, but at present no special simplification
1.8 -is performed.
1.9 +\isa{2 * 10\isacharcircum6}, which will be simplified to integers.
1.10
1.11 \begin{warn}
1.12 Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is