John Harrison: Verifying the Accuracy of Polynomial Approximations in HOL. TPHOLs 1997: 137-152