--- a/src/HOL/Main.thy Sun May 06 21:49:24 2007 +0200
+++ b/src/HOL/Main.thy Sun May 06 21:49:26 2007 +0200
@@ -5,17 +5,17 @@
header {* Main HOL *}
theory Main
-imports SAT ATP_Linkup
+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}.
*}
-text {* \medskip Late clause setup: installs \emph{all} known theorems
- into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
-
setup ResAxioms.setup
end