Isabelle's Metalogic: Formalization and Proof Checker.

Tobias Nipkow, Simon Rokopf

Browse the full CADE paper archive.