doc-src/TutorialI/Types/numerics.tex
 changeset 12333 ef43a3d6e962 parent 12156 d2758965362e child 13750 b5cd10cb106b
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Thu Nov 29 21:12:37 2001 +0100
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Nov 30 12:18:14 2001 +0100
1.3 @@ -424,7 +424,8 @@
1.4  defined for the reals, along with many theorems such as this one about
1.5  exponentiation:
1.6  \begin{isabelle}
1.7 -\isasymbar r\isasymbar \ \isacharcircum \ n\ =\ \isasymbar r\ \isacharcircum \ n\isasymbar
1.8 +\isasymbar r\ \isacharcircum \ n\isasymbar\ =\
1.9 +\isasymbar r\isasymbar \ \isacharcircum \ n
1.10  \rulename{realpow_abs}
1.11  \end{isabelle}
1.12
1.13 @@ -462,5 +463,8 @@
1.14  about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
1.15  development defines an infinitely large number, \isa{omega} and an
1.16  infinitely small positive number, \isa{epsilon}.  The
1.17 -relation $x\approx y$ means $x$ is infinitely close to~$y$''.%
1.18 +relation $x\approx y$ means $x$ is infinitely close to~$y$.''
1.19 +Theory \isa{Hyperreal} also defines transcendental functions such as sine,
1.20 +cosine, exponential and logarithm --- even the versions for type
1.21 +\isa{real}, because they are defined using nonstandard limits.%
1.22  \index{numbers|)}
1.23 \ No newline at end of file