Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive,
to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical є and
δ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet
rigorous, development of real analysis, and a relatively high degree of proof automation in many cases.