syst_float64_to_float32
float32 syst_float64_to_float32( float64 );
float64_to_float32, syst_float64_to_float32 );