(* Title: HOL/Main.thy ID: $Id$ *) header {* Main HOL *} theory Main imports Map begin text {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories. *} ML {* val HOL_proofs = ! Proofterm.proofs *} end