diff -r 3e30ea95c7aa -r 009ca4807baa CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 11 17:38:17 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Mar 11 22:34:49 2009 +0000
@@ -24,18 +24,18 @@
 ML{*val any = Scan.one (Symbol.not_eof)
 
 val scan_cmt =
-  let
-    val begin_cmt = Scan.this_string "(*" 
-    val end_cmt = Scan.this_string "*)"
-  in
-   begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 
-    >> (enclose "(**" "**)" o implode)
-  end
+let
+  val begin_cmt = Scan.this_string "(*" 
+  val end_cmt = Scan.this_string "*)"
+in
+  begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 
+  >> (enclose "(**" "**)" o implode)
+end
 
 val parser = Scan.repeat (scan_cmt || any)
 
 val scan_all =
-  Scan.finite Symbol.stopper parser >> implode #> fst *}
+      Scan.finite Symbol.stopper parser >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function 
@@ -95,6 +95,12 @@
 
 text {* \solution{ex:addconversion} *}
 
+text {*
+  The following code assumes the function @{ML dest_sum} from the previous
+  exercise.
+*}
+
+
 ML{*fun add_simple_conv ctxt ctrm =
 let
   val trm =  Thm.term_of ctrm
@@ -122,10 +128,14 @@
           Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i
   end)*}
 
+text {*
+  A test case is as follows
+*}
+
 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
+  where the conversion produces the goal state
   
   \begin{minipage}{\textwidth}
   @{subgoals [display]}