Also the spec does not state that ``real`` must be an 80-bit float.  But it's not worth changing the name of Tfloat80 at this point in time.