It's easy to describe:

echo odbc_result($ref, "column");
$a = (double) odbc_result($ref, "column");
echo "   /   " . $a;

output:

55.25   /   55

If I'm assigned result from odbc_result to some variable, it's ALWAYS convertet from DOUBLE to INTEGER.