--- a/CookBook/Tactical.thy	Wed Feb 25 21:55:08 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Feb 25 22:13:41 2009 +0000
@@ -1494,8 +1494,8 @@
   "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
   
   The conversion that goes under an application is
-  @{ML Conv.combination_conv}. It expects two conversions, which each of them
-  is applied to the corresponding ``branch'' of the application. 
+  @{ML Conv.combination_conv}. It expects two conversions as arguments, 
+  each of which is applied to the corresponding ``branch'' of the application. 
 
   We can now apply all these functions in a
   conversion that recursively descends a term and applies a conversion in all
@@ -1598,8 +1598,8 @@
   end)*}
 
 text {* 
-  We call the conversions with the argument @{ML "~1"} in order to 
-  analyse all parameters, premises and conclusions. If we call it with 
+  We call the conversions with the argument @{ML "~1"}. This is to 
+  analyse all parameters, premises and conclusions. If we call them with 
   a non-negative number, say @{text n}, then these conversions will 
   only be called on @{text n} premises (similar for parameters and
   conclusions). To test the tactic, consider the proof
@@ -1607,7 +1607,7 @@
 
 lemma
   "if True \<and> P then P else True \<and> False \<Longrightarrow>
-  (if True \<and> Q then Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
+  (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
 
@@ -1617,6 +1617,9 @@
 (*<*)oops(*>*)
 
 text {*
+  As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
+  the conclusion according to @{ML all_true1_conv}.
+
   To sum up this section, conversions are not as powerful as the simplifier
   and simprocs; the advantage of conversions, however, is that you never have
   to worry about non-termination.