  Isabelle is a generic theorem prover with a fragment of higher-order logic as
a metalogic for defining object logics. Isabelle also provides proof terms. We
formalize this metalogic and the language of proof terms in Isabelle/HOL,
define an executable (but inefficient) proof term checker and prove its
correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle
and run it on a range of logics and theories to check the correctness of all
the proofs in those theories.
