src/HOL/Main.thy
changeset 17721 b943c01e1c6d
parent 17618 1330157e156a
child 17905 1574533861b1
--- 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}. *}