summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 08 May 2003 15:23:21 +0200 | |

changeset 13983 | afc0dadddaa4 |

parent 13982 | 8abae6b7084c |

child 13984 | e055ba9020eb |

now refers to Complex and Complex_Main

--- a/doc-src/TutorialI/Types/numerics.tex Thu May 08 13:37:51 2003 +0200 +++ b/doc-src/TutorialI/Types/numerics.tex Thu May 08 15:23:21 2003 +0200 @@ -457,19 +457,19 @@ \begin{warn} -Type \isa{real} is only available in the logic HOL-Real, which -is HOL extended with a definitional development of the real +Type \isa{real} is only available in the logic HOL-Complex, which +is HOL extended with a definitional development of the real and complex numbers. Base your theory upon theory -\thydx{Real}, not the usual \isa{Main}.% +\thydx{Complex_Main}, not the usual \isa{Main}.% \index{real numbers|)}\index{*real (type)|)} Launch Isabelle using the command \begin{verbatim} -Isabelle -l HOL-Real +Isabelle -l HOL-Complex \end{verbatim} \end{warn} -Also distributed with Isabelle is HOL-Hyperreal, -whose theory \isa{Hyperreal} defines the type \tydx{hypreal} of +Also available in HOL-Complex is the +theory \isa{Hyperreal}, which define the type \tydx{hypreal} of \rmindex{non-standard reals}. These \textbf{hyperreals} include infinitesimals, which represent infinitely small and infinitely large quantities; they facilitate proofs