--- a/CookBook/Tactical.thy	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Feb 15 18:58:21 2009 +0000
@@ -56,7 +56,7 @@
   @{text xs} that will be generalised once the goal is proved (in our case
   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
   it can make use of the local assumptions (there are none in this example). 
-  The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to 
+  The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to 
   @{text erule}, @{text rule} and @{text assumption}, respectively. 
   The operator @{ML THEN} strings the tactics together. 
 
@@ -68,7 +68,7 @@
   Isabelle Reference Manual.
   \end{readmore}
 
-  Note that in the code above we used antiquotations for referencing the theorems. Many theorems
+  Note that in the code above we use 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 where there are no ML-binding obtain
   the theorem dynamically using the function @{ML thm}; for example 
@@ -309,7 +309,7 @@
   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
   "(C)"}. Since the goal @{term C} can potentially be an implication, there is
   a ``protector'' wrapped around it (in from of an outermost constant @{text
-  "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal; however this constant
+  "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
   is invisible in the figure). This prevents that premises of @{text C} are
   mis-interpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
@@ -952,7 +952,7 @@
 
 text {*
   is completely analysed according to the theorems we chose to
-  include in @{ML select_tac}. 
+  include in @{ML select_tac'}. 
 
   Recall that tactics produce a lazy sequence of successor goal states. These
   states can be explored using the command \isacommand{back}. For example
@@ -1015,8 +1015,13 @@
 
 text {*
   @{ML rewrite_goals_tac}
+  
   @{ML ObjectLogic.full_atomize_tac}
+  
   @{ML ObjectLogic.rulify_tac}
+
+  Something about simprocs.
+
 *}