src/HOL/Refute.thy
changeset 14463 ed09706ecc5d
parent 14457 6d5d6e78d851
child 14589 feae7b5fd425
     1.1 --- a/src/HOL/Refute.thy	Thu Mar 11 11:24:54 2004 +0100
     1.2 +++ b/src/HOL/Refute.thy	Thu Mar 11 13:03:31 2004 +0100
     1.3 @@ -17,7 +17,8 @@
     1.4  (* NOTE                                                                      *)
     1.5  (*                                                                           *)
     1.6  (* I strongly recommend that you install a stand-alone SAT solver if you     *)
     1.7 -(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.         *)
     1.8 +(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
     1.9 +(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'.        *)
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  
    1.12  (* ------------------------------------------------------------------------- *)
    1.13 @@ -33,18 +34,20 @@
    1.14  (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    1.15  (* equality), including free/bound/schematic variables, lambda abstractions, *)
    1.16  (* sets and set membership, "arbitrary", "The", and "Eps".  Constants for    *)
    1.17 -(* which a defining equation exists are unfolded automatically.              *)
    1.18 +(* which a defining equation exists are unfolded automatically.  Non-        *)
    1.19 +(* recursive inductive datatypes are supported.                              *)
    1.20 +(*                                                                           *)
    1.21 +(* The (space) complexity of the algorithm is exponential in both the length *)
    1.22 +(* of the formula and the size of the model.                                 *)
    1.23  (*                                                                           *)
    1.24  (* NOT (YET) SUPPORTED ARE                                                   *)
    1.25  (*                                                                           *)
    1.26  (* - schematic type variables                                                *)
    1.27 -(* - type constructors other than bool, =>, set                              *)
    1.28 -(* - other constants, including constructors of inductive datatypes,         *)
    1.29 -(*   inductively defined sets and recursive functions                        *)
    1.30 -(*                                                                           *)
    1.31 -(* For formulas that contain (variables of) an inductive datatype, a         *)
    1.32 -(* spurious countermodel may be returned.  Currently no warning is issued in *)
    1.33 -(* this case.                                                                *)
    1.34 +(* - axioms, sorts                                                           *)
    1.35 +(* - type constructors other than bool, =>, set, non-recursive IDTs          *)
    1.36 +(* - inductively defined sets                                                *)
    1.37 +(* - recursive functions                                                     *)
    1.38 +(* - ...                                                                     *)
    1.39  (* ------------------------------------------------------------------------- *)
    1.40  
    1.41  (* ------------------------------------------------------------------------- *)