changeset 108 | 8bea3f74889d |
parent 107 | 258ce361ba1b |
child 119 | 4536782969fa |
--- 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"}