# HG changeset patch
# User paulson
# Date 1258628316 0
# Node ID 15f9bd93a1ddd83d69bd125ae186800f6c57fe0d
# Parent  bc75dbbbf3e6c5dbc4d70502bbac69469daa0798
Minor correction

diff -r bc75dbbbf3e6 -r 15f9bd93a1dd doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 10:49:43 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 10:58:36 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