author | wenzelm |
Thu, 14 Sep 2006 15:51:20 +0200 | |
changeset 20537 | b6b49903db7e |
parent 20414 | 029c4f9dc6f4 |
child 21254 | d53f76357f41 |
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} known theorems into the clause cache; cf.\ theory @{text Reconstruction}. *} setup ResAxioms.setup end