syst_floatx80_to_float32
float32 syst_floatx80_to_float32( floatx80 );
floatx80_to_float32, syst_floatx80_to_float32 );