Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.

Johannes Hlzl, Fabian Immler, Brian Huffman

Browse the full ITP paper archive.