ProgTutorial/Recipes/TimeLimit.thy
changeset 191 0150cf5982ae
parent 189 069d525f8f1d
child 346 0fea8b7a14a1
equal deleted inserted replaced
190:ca0ac2e75f6d 191:0150cf5982ae
     6 
     6 
     7 text {*
     7 text {*
     8   {\bf Problem:}
     8   {\bf Problem:}
     9   Your tool should run only a specified amount of time.\smallskip
     9   Your tool should run only a specified amount of time.\smallskip
    10 
    10 
    11   {\bf Solution:} This can be achieved using the function 
    11   {\bf Solution:} In PolyML 5.2.1 and later, this can be achieved 
    12   @{ML timeLimit in TimeLimit}.\smallskip
    12   using the function @{ML timeLimit in TimeLimit}.\smallskip
    13 
    13 
    14   Assume you defined the Ackermann function on the ML-level.
    14   Assume you defined the Ackermann function on the ML-level.
    15 *}
    15 *}
    16 
    16 
    17 ML{*fun ackermann (0, n) = n + 1
    17 ML{*fun ackermann (0, n) = n + 1