John Harrison: Floating Point Verification in HOL. TPHOLs 1995: 186-199