--- a/CookBook/Solutions.thy	Fri Mar 13 01:15:55 2009 +0100
+++ b/CookBook/Solutions.thy	Fri Mar 13 12:21:44 2009 +0100
@@ -128,13 +128,13 @@
   end)*}
 
 text {*
-  A test case is as follows
+  A test case for this conversion is as follows
 *}
 
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
   apply(tactic {* add_tac 1 *})?
 txt {* 
-  where the conversion produces the goal state
+  where it produces the goal state
   
   \begin{minipage}{\textwidth}
   @{subgoals [display]}
@@ -202,7 +202,7 @@
 end*}
 
 text {*
-  This is all we need to let the conversion run against the simproc.
+  This is all we need to let the conversion run against the simproc:
 *}
 
 ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)