
diff -r 258ce361ba1b -r 8bea3f74889d CookBook/Intro.thy
--- a/CookBook/Intro.thy	Mon Feb 09 04:18:14 2009 +0000
+++ b/CookBook/Intro.thy	Wed Feb 11 17:40:24 2009 +0000
@@ -89,7 +89,7 @@
   
   Whenever appropriate we also show the response the code 
   generates when evaluated. This response is prefixed with a 
-  @{text [quotes] ">"} like:
+  @{text [quotes] ">"}, like:
 
   @{ML_response [display,gray] "3 + 4" "7"}
 




