author | wenzelm |
Tue, 17 Jul 2007 13:19:18 +0200 | |
changeset 23823 | 441148ca8323 |
parent 23165 | 5d319b0f8bf9 |
child 24632 | 779fc4fcbf8b |
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 ML {* val HOL_proofs = !proofs *} end