(* Title: HOL/Main.thy ID: $Id$*)header {* Main HOL *}theory Mainimports Mapbegintext {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories.*}ML {* val HOL_proofs = ! Proofterm.proofs *}ML {* path_add "~~/src/HOL/Library" *}end