--- a/src/HOL/Main.thy Thu Sep 29 15:50:43 2005 +0200
+++ b/src/HOL/Main.thy Thu Sep 29 15:50:44 2005 +0200
@@ -5,7 +5,7 @@
header {* Main HOL *}
theory Main
-imports Refute Reconstruction SAT
+imports SAT Reconstruction
begin
text {*
@@ -14,22 +14,7 @@
*}
-subsection {* Special hacks, late package setup etc. *}
-
-text {* \medskip Default values for refute, see also theory @{text
- Refute}.
-*}
-
-refute_params
- ["itself"=1,
- minsize=1,
- maxsize=8,
- maxvars=10000,
- maxtime=60,
- satsolver="auto"]
-
-
-text {* \medskip Clause setup: installs \emph{all} simprules and
+text {* \medskip Late clause setup: installs \emph{all} simprules and
claset rules into the clause cache; cf.\ theory @{text
Reconstruction}. *}