src/HOL/Tools/prop_logic.ML
changeset 14753 f40b45db8cf0
parent 14681 16fcef3a3174
child 14939 29fe4a9a7cb5
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Mon May 17 11:02:16 2004 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Mon May 17 14:05:06 2004 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  struct
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* prop_formula: formulas of propositional logic, built from boolean         *)
     1.8 +(* prop_formula: formulas of propositional logic, built from Boolean         *)
     1.9  (*               variables (referred to by index) and True/False using       *)
    1.10  (*               not/or/and                                                  *)
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 @@ -81,7 +81,7 @@
    1.13  	  | SAnd (fm1, fm2) = And (fm1, fm2);
    1.14  
    1.15  (* ------------------------------------------------------------------------- *)
    1.16 -(* indices: collects all indices of boolean variables that occur in a        *)
    1.17 +(* indices: collects all indices of Boolean variables that occur in a        *)
    1.18  (*      propositional formula 'fm'; no duplicates                            *)
    1.19  (* ------------------------------------------------------------------------- *)
    1.20  
    1.21 @@ -260,7 +260,7 @@
    1.22  	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
    1.23  
    1.24  (* ------------------------------------------------------------------------- *)
    1.25 -(* eval: given an assignment 'a' of boolean values to variable indices, the  *)
    1.26 +(* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
    1.27  (*      truth value of a propositional formula 'fm' is computed              *)
    1.28  (* ------------------------------------------------------------------------- *)
    1.29