author | krauss |
Thu, 17 May 2007 22:33:41 +0200 | |
changeset 22999 | c1ce129e6f9c |
parent 22840 | 643bb625a2c3 |
child 23165 | 5d319b0f8bf9 |
permissions | -rw-r--r-- |
(* Title: HOL/Main.thy ID: $Id$ *) header {* Main HOL *} theory Main imports Map Hilbert_Choice ATP_Linkup begin text {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories. \medskip Late clause setup: installs \emph{all} known theorems into the clause cache; cf.\ theory @{text ATP_Linkup}. *} setup ResAxioms.setup end