author | haftmann |
Wed, 22 Nov 2006 10:20:15 +0100 | |
changeset 21455 | b6be1d1b66c5 |
parent 21254 | d53f76357f41 |
child 22840 | 643bb625a2c3 |
permissions | -rw-r--r-- |
(* Title: HOL/Main.thy ID: $Id$ *) header {* Main HOL *} theory Main imports SAT ATP_Linkup 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 ATP_Linkup}. *} setup ResAxioms.setup end