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



We do have the full IEEE model:

https://www.isa-afp.org/entries/IEEE_Floating_Point.shtml <https://www.isa-afp.org/entries/IEEE_Floating_Point.shtml>

Larry Paulson


> On 2 Dec 2016, at 22:26, W. Douglas Maurer <maurer at email.gwu.edu> 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.