# HG changeset patch
# User haftmann
# Date 1178480966 -7200
# Node ID 643bb625a2c3e098b27a233619b01f75ce8bec76
# Parent  ede26eb5e549d0515e18a1e51cd002c644bcb5b6
minimal import

diff -r ede26eb5e549 -r 643bb625a2c3 src/HOL/Main.thy
--- 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