comments modified
authorwebertj
Wed Apr 28 10:45:35 2004 +0200 (2004-04-28)
changeset 1468116fcef3a3174
parent 14680 6029e76841fd
child 14682 a5072752114c
comments modified
src/HOL/Tools/prop_logic.ML
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Mon Apr 26 15:01:05 2004 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Wed Apr 28 10:45:35 2004 +0200
     1.3 @@ -20,11 +20,11 @@
     1.4  	val SOr  : prop_formula * prop_formula -> prop_formula
     1.5  	val SAnd : prop_formula * prop_formula -> prop_formula
     1.6  
     1.7 -	val indices : prop_formula -> int list  (* all variable indices *)
     1.8 +	val indices : prop_formula -> int list  (* set of all variable indices *)
     1.9  	val maxidx  : prop_formula -> int  (* maximal variable index *)
    1.10  
    1.11  	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
    1.12 -	val cnf    : prop_formula -> prop_formula  (* clause normal form *)
    1.13 +	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
    1.14  	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
    1.15  
    1.16  	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
    1.17 @@ -136,9 +136,9 @@
    1.18  	  | nnf (Not (Not fm))        = nnf fm;
    1.19  
    1.20  (* ------------------------------------------------------------------------- *)
    1.21 -(* cnf: computes the clause normal form (i.e. a conjunction of disjunctions) *)
    1.22 -(*      of a formula 'fm' of propositional logic.  The result formula may be *)
    1.23 -(*      exponentially longer than 'fm'.                                      *)
    1.24 +(* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
    1.25 +(*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
    1.26 +(*      formula may be exponentially longer than 'fm'.                       *)
    1.27  (* ------------------------------------------------------------------------- *)
    1.28  
    1.29  	(* prop_formula -> prop_formula *)
    1.30 @@ -175,10 +175,10 @@
    1.31  	end;
    1.32  
    1.33  (* ------------------------------------------------------------------------- *)
    1.34 -(* defcnf: computes the definitional clause normal form of a formula 'fm' of *)
    1.35 -(*      propositional logic, introducing auxiliary variables if necessary to *)
    1.36 -(*      avoid an exponential blowup of the formula.  The result formula is   *)
    1.37 -(*      satisfiable if and only if 'fm' is satisfiable.                      *)
    1.38 +(* defcnf: computes the definitional conjunctive normal form of a formula    *)
    1.39 +(*      'fm' of propositional logic, introducing auxiliary variables if      *)
    1.40 +(*      necessary to avoid an exponential blowup of the formula.  The result *)
    1.41 +(*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
    1.42  (* ------------------------------------------------------------------------- *)
    1.43  
    1.44  	(* prop_formula -> prop_formula *)