[isabelle] A small proof checker (String => Bool)

How could I go about obtaining a small proof checker for Isabelle HOL, that
takes a theory file and checks that it's valid? I would like it to be
simple to understand and as few lines of code as possible, yet it should
include the axioms of the system and be able to check the whole archive of
formal proofs.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.