--- a/ProgTutorial/FirstSteps.thy	Wed Aug 05 09:24:18 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 16:00:01 2009 +0200
@@ -147,7 +147,9 @@
   fun strip ("\^A" :: _ :: cs) = strip cs
     | strip (c :: cs) = c :: strip cs
     | strip [] = [];
-in implode o strip o explode end;
+in 
+  implode o strip o explode 
+end
 
 fun redirect_tracing stream =
  Output.tracing_fn := (fn s =>
@@ -268,14 +270,34 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
-  When printing out several `parcels' of information that belong 
-  together you should try to keep this information together. For 
-  this you can use the function @{ML [index] cat_lines}, which 
+  When printing out several parcels of information that semantiaclly 
+  belong  together, like a warning message consisting of a term and
+  a type, you should try to keep this information together 
+  in a single string. So do not print out information as
+
+@{ML_response_fake [display,gray]
+"tracing \"First half,\"; 
+tracing \"and second half.\""
+"First half,
+and second half."}
+
+  but as a single string with appropriate formatting. For example
+
+@{ML_response_fake [display,gray]
+"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"First half,
+and second half."}
+  
+  To ease this kind of string manipulations, there are a number
+  of library functions. For example,  the function @{ML [index] cat_lines}
   concatenates a list of strings and inserts newlines. 
 
   @{ML_response [display, gray]
   "cat_lines [\"foo\", \"bar\"]"
   "\"foo\\nbar\""}
+
+  Section \ref{sec:pretty} will also explain infrastructure that helps 
+  with more elaborate pretty printing. 
 *}