summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | webertj |

Thu, 11 Mar 2004 13:03:31 +0100 | |

changeset 14463 | ed09706ecc5d |

parent 14462 | e6550f190fe9 |

child 14464 | 72ad5f2a3803 |

Documentation updated

--- 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 *) +(* - ... *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *)