author | nipkow |
Sun, 09 Apr 2006 14:47:24 +0200 | |
changeset 19378 | 6cc9ac729eb5 |
parent 18510 | 0a6c24f549c3 |
child 19607 | 07eeb832f28d |
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