1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 11:57:30 2009 +0100
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 11:19:25 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