--- a/CookBook/Intro.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Intro.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -60,7 +60,8 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  to learn from that code.
+  to learn from that code. The UNIX command @{text "grep -R"} is
+  often your best friend while programming with Isabelle. 
   \end{description}
 
 *}
@@ -69,7 +70,7 @@
 
 text {*
 
-  All ML-code in this tutorial is typeset in highlighted boxes, like the following 
+  All ML-code in this tutorial is typeset in shaded boxes, like the following 
   ML-expression:
 
   \begin{isabelle}
@@ -96,10 +97,10 @@
 
   The user-level commands of Isabelle (i.e.~the non-ML code) are written
   in bold, for example \isacommand{lemma}, \isacommand{apply},
-  \isacommand{foobar} and so on.  We use @{text "$"} to indicate that a
+  \isacommand{foobar} and so on.  We use @{text "$ \<dots>"} to indicate that a
   command needs to be run in a Unix-shell, for example:
 
-  @{text [display] "$ ls -la"}
+  @{text [display] "$ grep -R ThyOutput *"}
 
   Pointers to further information and Isabelle files are typeset in 
   italic and highlighted as follows: