--- a/src/HOL/Tools/prop_logic.ML Mon May 17 11:02:16 2004 +0200
+++ b/src/HOL/Tools/prop_logic.ML Mon May 17 14:05:06 2004 +0200
@@ -38,7 +38,7 @@
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 *)
(* ------------------------------------------------------------------------- *)
@@ -81,7 +81,7 @@
| 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 *)
(* ------------------------------------------------------------------------- *)
@@ -260,7 +260,7 @@
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 *)
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/sat_solver.ML Mon May 17 11:02:16 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML Mon May 17 14:05:06 2004 +0200
@@ -230,8 +230,8 @@
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.solve "enumerate"' -- simply *)
-(* enumerates assignments until a satisfying assignment is found *)
+(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *)
+(* -- simply enumerates assignments until a satisfying assignment is found *)
(* ------------------------------------------------------------------------- *)
let
@@ -272,9 +272,9 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.solve "dpll"' -- a simple *)
-(* implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The Quest *)
-(* for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *)
+(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *)
+(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
+(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *)
(* ------------------------------------------------------------------------- *)
let
@@ -359,8 +359,8 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.solve "auto"': uses the *)
-(* first installed solver (other than "auto" itself) *)
+(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *)
+(* the first installed solver (other than "auto" itself) *)
(* ------------------------------------------------------------------------- *)
let