author | wenzelm |
Wed, 01 Feb 2006 22:20:40 +0100 | |
changeset 18888 | 3b643f81b378 |
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