*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Stefan Berghofer <berghofe at in.tum.de>*Subject*: [isabelle] Executing real numbers as approximating functions*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 08 Aug 2012 21:47:37 +0200*Organization*: TU Munich*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:14.0) Gecko/20120714 Thunderbird/14.0

Hi all, once I have heard about a formalisation to execute real numbers as approximating functions, i.e. where each real number r is implemented using a function R :: nat => float such that R n equals r approximated to the n-th digit (or something similar). Can somebody give me a reference for that? Thanks a lot, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Executing real numbers as approximating functions***From:*Brian Huffman

**Re: [isabelle] Executing real numbers as approximating functions***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Executing real numbers as approximating functions***From:*Freek Wiedijk

- Previous by Date: Re: [isabelle] Macro to comment and uncomment selected text so I don't get error?
- Next by Date: Re: [isabelle] Executing real numbers as approximating functions
- Previous by Thread: Re: [isabelle] Macro to comment and uncomment selected text so I don't get error?
- Next by Thread: Re: [isabelle] Executing real numbers as approximating functions
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list