On Arduino, double = float = 32 bits.

This is particularly annoying. I'd like to hack an Arduino based clock to display various Mars times, e.g. MTC and mission clocks for the rovers. The math I've found for this is straightforward, but it does operations involving small and large numbers. The tests I've done have made it clear that 32 bit float won't cut it, at least not unless I come up with a nifty way of rewriting all the equations.

Does anyone know of a library that can do basic arithmetic on 64 bit doubles? I don't even need trig. Add, subtract, multiply, divide, the ability to specify constants as 64 bit doubles, and the ability to convert between 32 bit floats and 64 bit doubles.

Thanks!