Re: [isabelle] Cl-isabelle-users Digest, Vol 138, Issue 4

We do have the full IEEE model: <>

Larry Paulson

> On 2 Dec 2016, at 22:26, W. Douglas Maurer <maurer at> wrote:
> Some day I hope it will be possible to implement a system that does what real computers do in this case: infinity minus infinity gives NaN, which stands for Not a Number. Then any combination of NaN with anything else also gives NaN. (See any formal description of IEEE standard floating point arithmetic.) --WDMaurer
> Sent from my iPhone

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.