--- a/CookBook/FirstSteps.thy	Thu Feb 05 22:40:46 2009 +0000
+++ b/CookBook/FirstSteps.thy	Thu Feb 05 22:44:11 2009 +0000
@@ -516,6 +516,59 @@
 
 section {* Theorem Attributes *}
 
+section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
+
+text {* 
+  It will often be necesseary to inspect terms, cterms or theorems. Isabelle
+  contains elaborate pretty-printing functions for that, but for quick-and-dirty
+  solutions they are too unwieldy. A term can be transformed into a string using
+  the function @{ML Syntax.string_of_term}
+
+  @{ML_response_fake [display,gray]
+  "Syntax.string_of_term @{context} @{term \"1::nat\"}"
+  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+
+  This produces a string, though with printing directions encoded in it. This
+  can be properly printed, when enclosed in a @{ML warning}
+
+  @{ML_response_fake [display,gray]
+  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "\"1\""}
+
+  A @{ML_type cterm} can be transformed into a string by the function:
+*}
+
+ML{*fun str_of_cterm ctxt t =  
+   Syntax.string_of_term ctxt (term_of t)*}
+
+text {*
+  If there are more than one @{ML_type cterm} to be printed, we can use the function
+  @{ML commas} to conveniently separate them.
+*} 
+
+ML{*fun str_of_cterms ctxt ts =  
+  commas (map (str_of_cterm ctxt) ts)*}
+
+text {*
+  The easiest way to get the string of a theorem, is to transform it
+  into a @{ML_type cterm} using the function @{ML crep_thm}.
+*}
+
+ML{*fun str_of_thm ctxt thm =
+  let
+    val {prop, ...} = crep_thm thm
+  in 
+    str_of_cterm ctxt prop
+  end*}
+
+text {* 
+  For more than one theorem, the following function adds commas in between them. 
+*}
+
+ML{*fun str_of_thms ctxt thms =  
+  commas (map (str_of_thm ctxt) thms)*}
+
+
 section {* Operations on Constants (Names) *}
 
 text {*
@@ -589,9 +642,10 @@
   the first component of the pair (Line 4) and finally incrementing the first 
   component by 4 (Line 5). This kind of cascading manipulations of values is quite
   common when dealing with theories (for example by adding a definition, followed by
-  lemmas and so on). It should also be familiar to anyone who has used Haskell's
-  do-notation. Writing the function @{ML inc_by_five} using the reverse
-  application is much clearer than writing
+  lemmas and so on). The reverse application allows you to read what happens inside
+  the function in a top-down manner. This kind of codeing should also be familiar, 
+  if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using 
+  the reverse application is much clearer than writing
 *}
 
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
@@ -648,8 +702,8 @@
   however, it uses @{ML tap} for printing the ``plus-one'' intermediate 
   result inside the tracing buffer. The function @{ML tap} can only
   be used for side-calculations, because any value that is computed cannot
-  be merged back into the ``main waterfall''. To do this, the next combinator
-  can be used.
+  be merged back into the ``main waterfall''. To do this, you can use the next 
+  combinator.
 
   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
   and returns the result together with the value (as a pair). For example
@@ -661,11 +715,10 @@
        |> (fn (x, y) => (x, y + 1))*}
 
 text {*
-  takes @{text x} as argument, and then first 
-  increments @{text x}, but also keeps @{text x}. The intermediate result is 
-  therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the 
-  right-hand component of the pair. So finally the result will be 
-  @{ML "(x + 1, x + 1)" for x}.
+  takes @{text x} as argument, and then increments @{text x}, but also keeps
+  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+  for x}. After that, the function increments the right-hand component of the
+  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
 
   The combinators @{ML "|>>"} and @{ML "||>"} are defined for 
   functions manipulating pairs. The first applies the function to