changeset 185 | 043ef82000b4 |
parent 184 | c7f04a008c9c |
child 186 | 371e4375c994 |
--- a/CookBook/FirstSteps.thy Wed Mar 18 03:03:51 2009 +0100 +++ b/CookBook/FirstSteps.thy Wed Mar 18 03:27:15 2009 +0100 @@ -897,8 +897,7 @@ shows "Q t" (*<*)oops(*>*) text {* - The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse - application. See Section~\ref{sec:combinators}.} + The corresponding ML-code is as follows: @{ML_response_fake [display,gray] "let