src/HOL/Tools/prop_logic.ML

 
 structure PropLogic : PROP_LOGIC =
 struct
 
 (* ------------------------------------------------------------------------- *)
-(* prop_formula: formulas of propositional logic, built from boolean         *)
+(* prop_formula: formulas of propositional logic, built from Boolean         *)
 (*               variables (referred to by index) and True/False using       *)
 (*               not/or/and                                                  *)
 (* ------------------------------------------------------------------------- *)
 
 	datatype prop_formula =

 	  | SAnd (False, _) = False
 	  | SAnd (_, False) = False
 	  | SAnd (fm1, fm2) = And (fm1, fm2);
 
 (* ------------------------------------------------------------------------- *)
-(* indices: collects all indices of boolean variables that occur in a        *)
+(* indices: collects all indices of Boolean variables that occur in a        *)
 (*      propositional formula 'fm'; no duplicates                            *)
 (* ------------------------------------------------------------------------- *)
 
 	(* prop_formula -> int list *)
 

 	(* prop_formula list * prop_formula list -> prop_formula *)
 
 	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
 
 (* ------------------------------------------------------------------------- *)
-(* eval: given an assignment 'a' of boolean values to variable indices, the  *)
+(* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
 (*      truth value of a propositional formula 'fm' is computed              *)
 (* ------------------------------------------------------------------------- *)
 
 	(* (int -> bool) -> prop_formula -> bool *)