ProgTutorial/Recipes/TimeLimit.thy
changeset 517 d8c376662bb4
parent 346 0fea8b7a14a1
child 557 77ea2de0ca62
equal deleted inserted replaced
516:fb6c29a90003 517:d8c376662bb4
    12   using the function @{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 %grayML{*fun ackermann (0, n) = n + 1
    18   | ackermann (m, 0) = ackermann (m - 1, 1)
    18   | ackermann (m, 0) = ackermann (m - 1, 1)
    19   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
    19   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
    20 
    20 
    21 text {*
    21 text {*
    22 
    22