(* Title: HOL/Main.thy ID: $Id: Main.thy,v 1.59 2005/09/29 13:50:44 wenzelm Exp $ *) header {* Main HOL *} theory Main imports SAT Reconstruction begin text {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories. *} text {* \medskip Late clause setup: installs \emph{all} simprules and claset rules into the clause cache; cf.\ theory @{text Reconstruction}. *} setup ResAxioms.clause_setup end