author | haftmann |
Wed, 07 Jun 2006 16:55:39 +0200 | |
changeset 19818 | 5c5c1208a3fa |
parent 19608 | 81fe44909dd5 |
child 20362 | bbff23c3e2ca |
permissions | -rw-r--r-- |
(* Title: HOL/Main.thy ID: $Id$ *) header {* Main HOL *} theory Main imports SAT Reconstruction ResAtpMethods 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.setup end