--- a/CookBook/Tactical.thy	Mon Mar 02 10:06:06 2009 +0000
+++ b/CookBook/Tactical.thy	Tue Mar 03 13:00:55 2009 +0000
@@ -289,8 +289,8 @@
   printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
   the goal state as represented internally (highlighted boxes). This
   illustrates that every goal state in Isabelle is represented by a theorem:
-  when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
-  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when we finish the proof the
+  when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
   theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
   \end{figure}
 *}
@@ -328,8 +328,9 @@
 
 text {*
   Let us start with the tactic @{ML print_tac}, which is quite useful for low-level 
-  debugging of tactics. It just prints out a message and the current goal state. 
-  Processing the proof
+  debugging of tactics. It just prints out a message and the current goal state 
+  (unlike @{ML my_print_tac} it prints the goal state as the user would see it). 
+  For example, processing the proof
 *}
  
 lemma shows "False \<Longrightarrow> True"
@@ -386,7 +387,7 @@
 
 text {*
   Note the number in each tactic call. Also as mentioned in the previous section, most 
-  basic tactics take such an argument; it addresses the subgoal they are analysing. 
+  basic tactics take such a number as argument; it addresses the subgoal they are analysing. 
   In the proof below, we first split up the conjunction in  the second subgoal by 
   focusing on this subgoal first.
 *}
@@ -692,10 +693,12 @@
   construct the patterns, the pattern in Line 8 cannot be constructed in this
   way. The reason is that an antiquotation would fix the type of the
   quantified variable. So you really have to construct the pattern using the
-  basic term-constructors. This is not necessary in other cases, because their type
-  is always fixed to function types involving only the type @{typ bool}. For the
-  final pattern, we chose to just return @{ML all_tac}. Consequently, 
-  @{ML select_tac} never fails.
+  basic term-constructors. This is not necessary in other cases, because their
+  type is always fixed to function types involving only the type @{typ
+  bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+  manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 
+  Consequently, @{ML select_tac} never fails.
+
 
   Let us now see how to apply this tactic. Consider the four goals:
 *}
@@ -924,7 +927,7 @@
   @{ML REPEAT1} is similar, but runs the tactic at least once (failing if 
   this is not possible).
 
-  If you are after the ``primed'' version of @{ML repeat_xmp} then you 
+  If you are after the ``primed'' version of @{ML repeat_xmp}, then you 
   need to implement it as
 *}