src/HOL/Tools/sat_solver.ML

 (* ------------------------------------------------------------------------- *)
 (* Predefined SAT solvers                                                    *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
-(* 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
 	fun enum_solver fm =
 	let

 in
 	SatSolver.add_solver ("enumerate", Some o enum_solver)
 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
 	local
 		open PropLogic

 in
 	SatSolver.add_solver ("dpll", Some o dpll_solver)
 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
 	fun auto_solver fm =
 		get_first (fn (name,solver) =>