80 bit reals

Henry Cejtin henry@sourcelight.com
Mon, 8 Oct 2001 15:30:39 -0500 

True, but it isn't clear that adding Real80 is worth much unless Real = Real64.