--- a/CookBook/Recipes/Sat.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -3,7 +3,7 @@
 imports Main "../Base"
 begin
 
-section {* SAT Solver\label{rec:sat} *}
+section {* SAT Solvers\label{rec:sat} *}
 
 text {*
   {\bf Problem:}
@@ -101,9 +101,9 @@
   The interface for the external SAT solvers is implemented
   in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple
   SAT solver based on the DPLL algorithm. The tactics for SAT solvers are
-  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"} Functions concerning
+  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning
   propositional formulas are implemented in @{ML_file
-  "HOL/Tools/prop_logic.ML"}. Tables used in the translation function are
+  "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
   implemented in @{ML_file "Pure/General/table.ML"}.  
   \end{readmore}
 *}