Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton's Principia

Demonstrations of Newton's theorems are usually presented using calculus. This text describes the mechanization of Lemmas and Propositions from the "Principia", using formal tools developed in the generic theorem prover Isabelle.