syst_float32_to_float64
float64 syst_float32_to_float64( float32 );
float32_to_float64, syst_float32_to_float64 );