--- a/CookBook/Intro.thy	Thu Feb 05 22:44:11 2009 +0000
+++ b/CookBook/Intro.thy	Fri Feb 06 06:19:52 2009 +0000
@@ -93,9 +93,10 @@
 
   @{ML_response [display,gray] "3 + 4" "7"}
 
-  The usual Isabelle commands are written in bold, for example \isacommand{lemma}, 
-  \isacommand{foobar} and so on.  We use @{text "$"} to indicate that 
-  a command  needs to be run in the Unix-shell, for example
+  The usual user-level commands of Isabelle are written in bold, for 
+  example \isacommand{lemma}, \isacommand{foobar} and so on.  
+  We use @{text "$"} to indicate that a command  needs to be run 
+  in the Unix-shell, for example
 
   @{text [display] "$ ls -la"}