--- a/CookBook/Solutions.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Solutions.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -148,7 +148,7 @@
   To measure any difference between the simproc and conversion, we will create 
   mechanically terms involving additions and then set up a goal to be 
   simplified. We have to be careful to set up the goal so that
-  other parts of the simplifier do not interfere. For this we set up an
+  other parts of the simplifier do not interfere. For this we construct an
   unprovable goal which, after simplification, we are going to ``prove'' with
   the help of the lemma:
 *}
@@ -175,7 +175,7 @@
 end*}
 
 text {*
-  This function generates for example
+  This function generates for example:
 
   @{ML_response_fake [display,gray] 
   "warning (Syntax.string_of_term @{context} (term_tree 2))" 
@@ -191,7 +191,7 @@
   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
   respectively. The idea is to first apply the conversion (respectively simproc) and 
-  then prove the remaining goal using the lemma @{thm [source] cheat}.
+  then prove the remaining goal using the @{thm [source] cheat}-lemma.
 *}
 
 ML{*local
@@ -210,7 +210,7 @@
 
 text {*
   If you do the exercise, you can see that both ways of simplifying additions
-  perform relatively the same with perhaps some advantages for the
+  perform relatively similar with perhaps some advantages for the
   simproc. That means the simplifier, even if much more complicated than
   conversions, is quite efficient for tasks it is designed for. It usually does not
   make sense to implement general-purpose rewriting using