Type classes and filters for mathematical analysis in Isabelle/HOL
ITP, pp. 279-294, 2013.
extended real numberalgebraic spacegeneric theorybounded continuous functiontype classMore(7+)
The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, ℂ and ℝn. Isabelle's new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of ...More
Full Text (Upload PDF)
PPT (Upload PPT)