--- a/src/HOL/Refute.thy Wed May 26 18:03:52 2004 +0200
+++ b/src/HOL/Refute.thy Wed May 26 18:06:38 2004 +0200
@@ -32,7 +32,8 @@
(* *)
(* 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'. If you *)
-(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'. *)
+(* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in *)
+(* 'etc/settings'. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
@@ -47,20 +48,18 @@
(* *)
(* '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. Non- *)
-(* recursive inductive datatypes are supported. *)
+(* sets and set membership, "arbitrary", "The", and "Eps". Defining *)
+(* equations for constants are added automatically. Inductive datatypes are *)
+(* supported, but may lead to spurious countermodels. *)
(* *)
-(* The (space) complexity of the algorithm is exponential in both the length *)
-(* of the formula and the size of the model. *)
+(* The (space) complexity of the algorithm is non-elementary. *)
(* *)
(* NOT (YET) SUPPORTED ARE *)
(* *)
(* - schematic type variables *)
(* - axioms, sorts *)
-(* - type constructors other than bool, =>, set, non-recursive IDTs *)
(* - inductively defined sets *)
-(* - recursive functions *)
+(* - recursive functions on IDTs (case, recursion operators, size) *)
(* - ... *)
(* ------------------------------------------------------------------------- *)
@@ -78,9 +77,16 @@
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
(* when transforming the term into a propositional *)
(* formula. *)
+(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
+(* This value is ignored under some ML compilers. *)
(* "satsolver" string Name of the SAT solver to be used. *)
(* *)
(* See 'HOL/Main.thy' for default values. *)
+(* *)
+(* The size of particular types can be specified in the form type=size *)
+(* (where 'type' is a string, and 'size' is an int). Examples: *)
+(* "'a"=1 *)
+(* "List.list"=2 *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
@@ -89,7 +95,7 @@
(* HOL/Tools/prop_logic.ML Propositional logic *)
(* HOL/Tools/sat_solver.ML SAT solvers *)
(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
-(* boolean assignment -> HOL model *)
+(* Boolean assignment -> HOL model *)
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
(* syntax *)
(* HOL/Refute.thy This file: loads the ML files, basic setup, *)