--- a/CookBook/Solutions.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/Solutions.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -1,5 +1,6 @@
 theory Solutions
 imports Base
+uses "infix_conv.ML"
 begin
 
 chapter {* Solutions to Most Exercises *}
@@ -90,9 +91,50 @@
   
   \begin{minipage}{\textwidth}
   @{subgoals [display]}
-  \end{minipage}
+  \end{minipage}\bigskip
+*}(*<*)oops(*>*)
+
+text {* \solution{ex:addconversion} *}
+
+text {*
+  (FIXME This solution works but is awkward.)
+*}
+
+ML{*fun add_conv ctxt ctrm =
+  (case Thm.term_of ctrm of
+     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
+         (let
+            val eq1 = Conv.binop_conv (add_conv ctxt) ctrm;
+            val ctrm' = Thm.rhs_of eq1;
+            val trm' = Thm.term_of ctrm';
+            val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm'
+          in
+             Thm.transitive eq1 eq2
+          end)       
+    | _ $ _ => Conv.combination_conv 
+                 (add_conv ctxt) (add_conv ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm)
+
+val add_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 (add_conv ctxt) then_conv
+          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i
+  end)*}
+
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+  apply(tactic {* add_tac 1 *})?
+txt {* 
+  where the simproc produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
 
-
 end
\ No newline at end of file