(* Title: HOL/Main.thy ID: $Id$ *) header {* Main HOL *} theory Main imports Plain Map Presburger Recdef begin ML {* val HOL_proofs = ! Proofterm.proofs *} text {* See further \cite{Nipkow-et-al:2002:tutorial} *} end