--- a/CookBook/Tactical.thy	Tue Feb 24 01:30:15 2009 +0000
+++ b/CookBook/Tactical.thy	Tue Feb 24 11:15:41 2009 +0000
@@ -1025,7 +1025,7 @@
 text {*
   In Isabelle you can also implement custom simplification procedures, called
   \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
-  rewrite a term according to theorem. They are useful in cases where
+  rewrite a term according to a theorem. They are useful in cases where
   a rewriting rule must be produced on ``demand'' or when rewriting by
   simplification is too unpredictable and potentially loops.
 
@@ -1232,7 +1232,7 @@
   @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
   (Line 4), which it proves by the arithmetic tactic in Line 6. 
 
-  For our purpose at the moment, using in the code above @{ML arith_tac} is
+  For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
   fine, but there is also an alternative employing the simplifier with a very
   restricted simpset. For the kind of lemmas we want to prove, the simpset
   @{text "num_ss"} in the code will suffice.