--- a/CookBook/Tactical.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/Tactical.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -137,14 +137,14 @@
 
   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
-  of this form, then they return the error message:
+  of this form, then these tactics return the error message:
 
   \begin{isabelle}
   @{text "*** empty result sequence -- proof command failed"}\\
   @{text "*** At command \"apply\"."}
   \end{isabelle}
 
-  This means the tactics failed. The reason for this error message is that tactics 
+  This means they failed. The reason for this error message is that tactics 
   are functions mapping a goal state to a (lazy) sequence of successor states. 
   Hence the type of a tactic is:
 *}
@@ -423,7 +423,7 @@
 (*<*)oops(*>*)
 
 text {* 
-  Similarl versions taking a list of theorems exist for the tactics 
+  Similar versions taking a list of theorems exist for the tactics 
   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
 
 
@@ -677,7 +677,7 @@
 
 text {*
   The input of the function is a term representing the subgoal and a number
-  specifying the subgoal of interest. In line 3 you need to descend under the
+  specifying the subgoal of interest. In Line 3 you need to descend under the
   outermost @{term "Trueprop"} in order to get to the connective you like to
   analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
   analysed. Similarly with meta-implications in the next line.  While for the
@@ -1154,9 +1154,9 @@
 \end{figure} *}
 
 text {* 
-  To see how they work, consider the two functions in Figure~\ref{fig:printss}, which
-  print out some parts of a simpset. If you use them to print out the components of the
-  empty simpset, in ML @{ML empty_ss} and the most primitive simpset
+  To see how they work, consider the function in Figure~\ref{fig:printss}, which
+  prints out some parts of a simpset. If you use it to print out the components of the
+  empty simpset, i.e.~ @{ML empty_ss}
   
   @{ML_response_fake [display,gray]
   "print_ss @{context} empty_ss"
@@ -1214,7 +1214,12 @@
 
   also produces ``nothing'', the printout is misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
-  form  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]}; 
+  form  
+
+  \begin{isabelle}
+  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]}; 
+  \end{isabelle}
+
   and also resolve with assumptions. For example:
 *}
 
@@ -1225,9 +1230,7 @@
 
 text {*
   This behaviour is not because of simplification rules, but how the subgoaler, solver 
-  and looper are set up. @{ML HOL_basic_ss} is usually a good start to build your 
-  own simpsets, because of the low danger of causing loops via interacting simplifiction
-  rules.
+  and looper are set up in @{ML HOL_basic_ss}.
 
   The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing 
   already many useful simplification and congruence rules for the logical 
@@ -1255,10 +1258,14 @@
 
 definition "MyTrue \<equiv> True"
 
+text {*
+  then in the following proof we can unfold this constant
+*}
+
 lemma shows "MyTrue \<Longrightarrow> True \<and> True"
 apply(rule conjI)
 apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
-txt{* then the tactic produces the goal state
+txt{* producing the goal state
 
       \begin{minipage}{\textwidth}
       @{subgoals [display]}
@@ -1737,7 +1744,7 @@
   to theorems via tactics. The type for conversions is
 *}
 
-ML{*type conv = Thm.cterm -> Thm.thm*}
+ML{*type conv = cterm -> thm*}
 
 text {*
   whereby the produced theorem is always a meta-equality. A simple conversion
@@ -2009,15 +2016,11 @@
   Here is a tactic doing exactly that:
 *}
 
-ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
-  let 
-    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
-  in
-    CONVERSION 
-      (Conv.params_conv ~1 (fn ctxt =>
-        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
-          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i
-  end)*}
+ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
+  CONVERSION 
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
+          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i)*}
 
 text {* 
   We call the conversions with the argument @{ML "~1"}. This is to 
@@ -2030,7 +2033,7 @@
 lemma
   "if True \<and> P then P else True \<and> False \<Longrightarrow>
   (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
-apply(tactic {* true1_tac 1 *})
+apply(tactic {* true1_tac @{context} 1 *})
 txt {* where the tactic yields the goal state
 
   \begin{minipage}{\textwidth}