--- a/CookBook/FirstSteps.thy Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/FirstSteps.thy Fri Feb 13 09:57:08 2009 +0000
@@ -643,7 +643,7 @@
the purpose of this combinator is to implement functions in a
``waterfall fashion''. Consider for example the function *}
-ML %linenumbers{*fun inc_by_five x =
+ML %linenosgray{*fun inc_by_five x =
x |> (fn x => x + 1)
|> (fn x => (x, x))
|> fst
@@ -706,7 +706,7 @@
*}
-ML %linenumbers{*fun inc_by_three x =
+ML %linenosgray{*fun inc_by_three x =
x |> (fn x => x + 1)
|> tap (fn x => tracing (makestring x))
|> (fn x => x + 2)*}