src/HOL/Refute.thy
changeset 15293 7797a04cc188
parent 15140 322485b816ac
child 16417 9bc16273c2d4
equal deleted inserted replaced
15292:09e218879265 15293:7797a04cc188
    31 (* ------------------------------------------------------------------------- *)
    31 (* ------------------------------------------------------------------------- *)
    32 (* NOTE                                                                      *)
    32 (* NOTE                                                                      *)
    33 (*                                                                           *)
    33 (*                                                                           *)
    34 (* I strongly recommend that you install a stand-alone SAT solver if you     *)
    34 (* I strongly recommend that you install a stand-alone SAT solver if you     *)
    35 (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
    35 (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
    36 (* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in     *)
    36 (* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
    37 (* 'etc/settings'.                                                           *)
    37 (* in 'etc/settings'.                                                        *)
    38 (* ------------------------------------------------------------------------- *)
    38 (* ------------------------------------------------------------------------- *)
    39 
    39 
    40 (* ------------------------------------------------------------------------- *)
    40 (* ------------------------------------------------------------------------- *)
    41 (* USAGE                                                                     *)
    41 (* USAGE                                                                     *)
    42 (*                                                                           *)
    42 (*                                                                           *)