--- a/doc-src/TutorialI/Types/numerics.tex Thu Nov 19 11:57:30 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Thu Nov 19 11:19:25 2009 +0000
@@ -347,8 +347,7 @@
\ 1.\ P\ (2\ /\ 5)
\end{isabelle}
Exponentiation can express floating-point values such as
-\isa{2 * 10\isacharcircum6}, but at present no special simplification
-is performed.
+\isa{2 * 10\isacharcircum6}, which will be simplified to integers.
\begin{warn}
Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is