--- a/CookBook/Tactical.thy	Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Tactical.thy	Sat Feb 14 13:20:21 2009 +0000
@@ -70,7 +70,7 @@
 
   Note that in the code above we used antiquotations for referencing the theorems. Many theorems
   also have ML-bindings with the same name. Therefore, we could also just have
-  written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
+  written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
   the theorem dynamically using the function @{ML thm}; for example 
   \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 
   The reason
@@ -284,9 +284,13 @@
 done
 text_raw {*  
   \end{isabelle}
-  \caption{A proof where we show the goal state as printed 
-  by the Isabelle system and as represented internally 
-  (highlighted boxes).\label{fig:goalstates}}
+  \caption{The figure shows a proof where each intermediate goal state is
+  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
+  theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
   \end{figure}
 *}
 
@@ -443,7 +447,7 @@
 *}
 
 lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
-apply(drule bspec)
+apply(tactic {* dtac @{thm bspec} 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]} 
      \end{minipage}*}
@@ -595,7 +599,7 @@
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 
 txt {*
-  then tactic prints out 
+  then the tactic prints out: 
 
   \begin{quote}\small
   \begin{tabular}{ll}
@@ -687,7 +691,7 @@
   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}. The
+  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.
 
@@ -784,7 +788,7 @@
                        atac, rtac @{thm disjI1}, atac]*}
 
 text {*
-  and just call @{ML foo_tac1}.  
+  and call @{ML foo_tac1}.  
 
   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
   guaranteed that all component tactics successfully apply; otherwise the
@@ -824,7 +828,7 @@
 text {*
   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
   we must include @{ML all_tac} at the end of the list, otherwise the tactic will
-  fail if no rule applies (we laso have to wrap @{ML all_tac} using the 
+  fail if no rule applies (we also have to wrap @{ML all_tac} using the 
   @{ML K}-combinator, because it does not take a subgoal number as argument). You can 
   test the tactic on the same goals:
 *}
@@ -992,7 +996,7 @@
       \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-  This will combinator prune the search space to just the first successful application.
+  This combinator will prune the search space to just the first successful application.
   Attempting to apply \isacommand{back} in this goal states gives the
   error message: