src/HOL/Main.thy
changeset 14350 41b32020d0b3
parent 14192 d6cb80cc1d20
child 14443 75910c7557c5
     1.1 --- a/src/HOL/Main.thy	Sat Jan 10 12:34:50 2004 +0100
     1.2 +++ b/src/HOL/Main.thy	Sat Jan 10 13:35:10 2004 +0100
     1.3 @@ -1,12 +1,12 @@
     1.4  (*  Title:      HOL/Main.thy
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.7 +    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     1.8      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  *)
    1.10  
    1.11  header {* Main HOL *}
    1.12  
    1.13 -theory Main = Map + Hilbert_Choice + Extraction:
    1.14 +theory Main = Map + Hilbert_Choice + Extraction + Refute:
    1.15  
    1.16  text {*
    1.17    Theory @{text Main} includes everything.  Note that theory @{text
    1.18 @@ -91,4 +91,26 @@
    1.19  lemma [code]: "(0 < Suc n) = True" by simp
    1.20  lemmas [code] = Suc_less_eq imp_conv_disj
    1.21  
    1.22 +subsection {* Configuration of the 'refute' command *}
    1.23 +
    1.24 +text {*
    1.25 +  The following are reasonable default parameters (for use with
    1.26 +  ZChaff 2003.12.04).  For an explanation of these parameters,
    1.27 +  see 'HOL/Refute.thy'.
    1.28 +
    1.29 +  \emph{Note}: If you want to use a different SAT solver (or
    1.30 +  install ZChaff to a different location), you will need to
    1.31 +  override at least the values for 'command' and (probably)
    1.32 +  'success' in your own theory file.
    1.33 +*}
    1.34 +
    1.35 +refute_params [minsize=1,
    1.36 +               maxsize=8,
    1.37 +               maxvars=200,
    1.38 +               satfile="refute.cnf",
    1.39 +               satformat="defcnf",
    1.40 +               resultfile="refute.out",
    1.41 +               success="Verify Solution successful. Instance satisfiable",
    1.42 +               command="$HOME/bin/zchaff refute.cnf 60 > refute.out"]
    1.43 +
    1.44  end