Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL