diff -r ca0ac2e75f6d -r 0150cf5982ae ProgTutorial/Recipes/TimeLimit.thy --- a/ProgTutorial/Recipes/TimeLimit.thy Thu Mar 19 17:50:28 2009 +0100 +++ b/ProgTutorial/Recipes/TimeLimit.thy Thu Mar 19 23:21:26 2009 +0100 @@ -8,8 +8,8 @@ {\bf Problem:} Your tool should run only a specified amount of time.\smallskip - {\bf Solution:} This can be achieved using the function - @{ML timeLimit in TimeLimit}.\smallskip + {\bf Solution:} In PolyML 5.2.1 and later, this can be achieved + using the function @{ML timeLimit in TimeLimit}.\smallskip Assume you defined the Ackermann function on the ML-level. *}