# HG changeset patch
# User wenzelm
# Date 1258632016 -3600
# Node ID b1fbd5f3cfb4e56161861cb111b5b8dbbd367abf
# Parent  00ef1f08ad58639a9ebe3be955f6604f976b1786# Parent  982661194362fb2bae2b46604d91301be6d1baef
merged

diff -r 982661194362 -r b1fbd5f3cfb4 doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 12:59:32 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu Nov 19 13:00:16 2009 +0100
@@ -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