 Since arguments using infinitesimals are usually easier to visualise than arguments using limits, nonstandard analysis is a helpful tool for mathematical analysts. Jacques Fleuriot in his Ph.D. thesis (2001) automated the proof theory of nonstandard analysis and used it to mechanise some of the proofs in Newton’s Principia.