--- a/CookBook/Tactical.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -662,17 +662,20 @@
   also described in \isccite{sec:results}. 
   \end{readmore}
 
-  A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. 
-  It allows you to inspect a given  subgoal. With this you can implement 
-  a tactic that applies a rule according to the topmost logic connective in the 
-  subgoal (to illustrate this we only analyse a few connectives). The code
-  of the tactic is as follows.\label{tac:selecttac}
+  Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
+  and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
+  presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
+  cterm}). With this you can implement a tactic that applies a rule according
+  to the topmost logic connective in the subgoal (to illustrate this we only
+  analyse a few connectives). The code of the tactic is as
+  follows.\label{tac:selecttac}
+
 *}
 
-ML %linenosgray{*fun select_tac (t,i) =
+ML %linenosgray{*fun select_tac (t, i) =
   case t of
-     @{term "Trueprop"} $ t' => select_tac (t',i)
-   | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)
+     @{term "Trueprop"} $ t' => select_tac (t', i)
+   | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
    | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
    | @{term "Not"} $ _ => rtac @{thm notI} i
@@ -727,8 +730,7 @@
   the first goal. To do this can result in quite messy code. In contrast, 
   the ``reverse application'' is easy to implement.
 
-  The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes
-  a @{ML_type cterm} instead of a @{ML_type term}.  Of course, this example is
+  Of course, this example is
   contrived: there are much simpler methods available in Isabelle for
   implementing a proof procedure analysing a goal according to its topmost
   connective. These simpler methods use tactic combinators, which we will
@@ -1013,7 +1015,7 @@
 
 *}
 
-section {* Rewriting and Simplifier Tactics *}
+section {* Simplifier Tactics *}
 
 text {*
   @{ML rewrite_goals_tac}
@@ -1458,7 +1460,7 @@
 
   Here the conversion of @{thm [source] true_conj1} only applies
   in the first case, but fails in the second. The whole conversion
-  does not fail, however, because the combinator @{ML else_conv} will then 
+  does not fail, however, because the combinator @{ML Conv.else_conv} will then 
   try out @{ML Conv.all_conv}, which always succeeds.
 
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
@@ -1600,8 +1602,8 @@
   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
+        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
+          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i
   end)*}
 
 text {* 
@@ -1629,15 +1631,23 @@
   and simprocs; the advantage of conversions, however, is that you never have
   to worry about non-termination.
 
+  \begin{exercise}\label{ex:addconversion}
+  Write a tactic that is based on conversions which does the same as the simproc in
+  exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} 
+  by their result. You can make the same assumptions as in \ref{ex:addsimproc}.
+  \end{exercise}
+
   \begin{readmore}
   See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 
   Further conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
   \end{readmore}
+
 *}
 
 
 
+
 section {* Structured Proofs *}
 
 text {* TBD *}