# HG changeset patch
# User webertj
# Date 1083141935 -7200
# Node ID 16fcef3a317468d4c0be280e62fdb0fbbfe8cf15
# Parent  6029e76841fd4acd780338d6e040ef723dff5228
comments modified

diff -r 6029e76841fd -r 16fcef3a3174 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Mon Apr 26 15:01:05 2004 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Wed Apr 28 10:45:35 2004 +0200
@@ -20,11 +20,11 @@
 	val SOr  : prop_formula * prop_formula -> prop_formula
 	val SAnd : prop_formula * prop_formula -> prop_formula
 
-	val indices : prop_formula -> int list  (* all variable indices *)
+	val indices : prop_formula -> int list  (* set of all variable indices *)
 	val maxidx  : prop_formula -> int  (* maximal variable index *)
 
 	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
-	val cnf    : prop_formula -> prop_formula  (* clause normal form *)
+	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
 	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
 
 	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
@@ -136,9 +136,9 @@
 	  | nnf (Not (Not fm))        = nnf fm;
 
 (* ------------------------------------------------------------------------- *)
-(* cnf: computes the clause normal form (i.e. a conjunction of disjunctions) *)
-(*      of a formula 'fm' of propositional logic.  The result formula may be *)
-(*      exponentially longer than 'fm'.                                      *)
+(* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
+(*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
+(*      formula may be exponentially longer than 'fm'.                       *)
 (* ------------------------------------------------------------------------- *)
 
 	(* prop_formula -> prop_formula *)
@@ -175,10 +175,10 @@
 	end;
 
 (* ------------------------------------------------------------------------- *)
-(* defcnf: computes the definitional clause normal form of a formula 'fm' of *)
-(*      propositional logic, introducing auxiliary variables if necessary to *)
-(*      avoid an exponential blowup of the formula.  The result formula is   *)
-(*      satisfiable if and only if 'fm' is satisfiable.                      *)
+(* defcnf: computes the definitional conjunctive normal form of a formula    *)
+(*      'fm' of propositional logic, introducing auxiliary variables if      *)
+(*      necessary to avoid an exponential blowup of the formula.  The result *)
+(*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
 (* ------------------------------------------------------------------------- *)
 
 	(* prop_formula -> prop_formula *)