# HG changeset patch
# User webertj
# Date 1078954653 -3600
# Node ID c2b96948730d41e6291013fc28255ff57ae02797
# Parent  6d5d6e78d8519b0eb2ecfbb4205e93cece5371e0
changed default values for refute

diff -r 6d5d6e78d851 -r c2b96948730d src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Mar 10 22:35:37 2004 +0100
+++ b/src/HOL/Main.thy	Wed Mar 10 22:37:33 2004 +0100
@@ -94,23 +94,13 @@
 subsection {* Configuration of the 'refute' command *}
 
 text {*
-  The following are reasonable default parameters (for use with
-  ZChaff 2003.12.04).  For an explanation of these parameters,
-  see 'HOL/Refute.thy'.
-
-  \emph{Note}: If you want to use a different SAT solver (or
-  install ZChaff to a different location), you will need to
-  override at least the values for 'command' and (probably)
-  'success' in your own theory file.
+  The following are fairly reasonable default values.  For an
+  explanation of these parameters, see 'HOL/Refute.thy'.
 *}
 
 refute_params [minsize=1,
                maxsize=8,
-               maxvars=200,
-               satfile="refute.cnf",
-               satformat="defcnf",
-               resultfile="refute.out",
-               success="Verify Solution successful. Instance satisfiable",
-               command="$HOME/bin/zchaff refute.cnf 60 > refute.out"]
+               maxvars=100,
+               satsolver="auto"]
 
 end