# HG changeset patch
# User webertj
# Date 1079006611 -3600
# Node ID ed09706ecc5d4b704fce863e4cb65e715fa50ee8
# Parent  e6550f190fe9698d167ec6d657da1c1a5d564a54
Documentation updated

diff -r e6550f190fe9 -r ed09706ecc5d src/HOL/Refute.thy
--- 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                                                     *)
+(* - ...                                                                     *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)