# HG changeset patch # User paulson # Date 1258629565 0 # Node ID 00ef1f08ad58639a9ebe3be955f6604f976b1786 # Parent b369324fc244c6a6ef3ce950be48ef3889138eb4# Parent 15f9bd93a1ddd83d69bd125ae186800f6c57fe0d merged diff -r b369324fc244 -r 00ef1f08ad58 doc-src/TutorialI/Types/numerics.tex --- 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