--- a/src/HOL/Refute.thy Thu Mar 11 11:24:54 2004 +0100
+++ b/src/HOL/Refute.thy Thu Mar 11 13:03:31 2004 +0100
@@ -17,7 +17,8 @@
(* NOTE *)
(* *)
(* I strongly recommend that you install a stand-alone SAT solver if you *)
-(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. *)
+(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *)
+(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
@@ -33,18 +34,20 @@
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
(* equality), including free/bound/schematic variables, lambda abstractions, *)
(* sets and set membership, "arbitrary", "The", and "Eps". Constants for *)
-(* which a defining equation exists are unfolded automatically. *)
+(* which a defining equation exists are unfolded automatically. Non- *)
+(* recursive inductive datatypes are supported. *)
+(* *)
+(* The (space) complexity of the algorithm is exponential in both the length *)
+(* of the formula and the size of the model. *)
(* *)
(* NOT (YET) SUPPORTED ARE *)
(* *)
(* - schematic type variables *)
-(* - type constructors other than bool, =>, set *)
-(* - other constants, including constructors of inductive datatypes, *)
-(* inductively defined sets and recursive functions *)
-(* *)
-(* For formulas that contain (variables of) an inductive datatype, a *)
-(* spurious countermodel may be returned. Currently no warning is issued in *)
-(* this case. *)
+(* - axioms, sorts *)
+(* - type constructors other than bool, =>, set, non-recursive IDTs *)
+(* - inductively defined sets *)
+(* - recursive functions *)
+(* - ... *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)