# HG changeset patch
# User webertj
# Date 1168475663 -3600
# Node ID 49faa8c7a5d99a6ce5e7089a80205dc31a4c0cba
# Parent  d7c91b2f5a9e95991645e0e2ff6d5ebddf38e6f7
updated to mention the automatic unfolding of constants

diff -r d7c91b2f5a9e -r 49faa8c7a5d9 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Wed Jan 10 20:17:26 2007 +0100
+++ b/src/HOL/Refute.thy	Thu Jan 11 01:34:23 2007 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Refute.thy
     ID:         $Id$
     Author:     Tjark Weber
-    Copyright   2003-2005
+    Copyright   2003-2007
 
 Basic setup and documentation for the 'refute' (and 'refute_params') command.
 *)
@@ -50,10 +50,10 @@
 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
 (* equality), including free/bound/schematic variables, lambda abstractions, *)
 (* sets and set membership, "arbitrary", "The", "Eps", records and           *)
-(* inductively defined sets.  Defining equations for constants are added     *)
-(* automatically, as are sort axioms.  Other, user-asserted axioms however   *)
-(* are ignored.  Inductive datatypes and recursive functions are supported,  *)
-(* but may lead to spurious countermodels.                                   *)
+(* inductively defined sets.  Constants are unfolded automatically, and sort *)
+(* axioms are added as well.  Other, user-asserted axioms however are        *)
+(* ignored.  Inductive datatypes and recursive functions are supported, but  *)
+(* may lead to spurious countermodels.                                       *)
 (*                                                                           *)
 (* The (space) complexity of the algorithm is non-elementary.                *)
 (*                                                                           *)