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