src/HOL/Tools/prop_logic.ML
changeset 16913 1d8a8d010e69
parent 16909 acbc7a9c3864
child 17809 195045659c06
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Jul 26 12:40:52 2005 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Jul 26 14:14:13 2005 +0200
     1.3 @@ -224,10 +224,11 @@
     1.4  
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  (* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
     1.7 -(*      'defcnf' below, but sometimes generates slightly larger SAT problems *)
     1.8 +(*      'defcnf' below, but sometimes generates much larger SAT problems     *)
     1.9  (*      overall (hence it must sometimes generate longer clauses than        *)
    1.10  (*      'defcnf' does).  It is currently not quite clear to me if one of the *)
    1.11 -(*      algorithms is clearly superior to the other.                         *)
    1.12 +(*      algorithms is clearly superior to the other, but I suggest using     *)
    1.13 +(*      'defcnf' instead.                                                    *)
    1.14  (* ------------------------------------------------------------------------- *)
    1.15  
    1.16  	(* prop_formula -> prop_formula *)