CookBook/FirstSteps.thy
changeset 114 13fd0a83d3c3
parent 108 8bea3f74889d
child 118 5f003fdf2653
--- 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)*}