CookBook/Recipes/TimeLimit.thy
changeset 69 19106a9975c1
parent 68 e7519207c2b7
child 72 7b8c4fe235aa
equal deleted inserted replaced
68:e7519207c2b7 69:19106a9975c1
    13 
    13 
    14   Assume you defined the Ackermann function:
    14   Assume you defined the Ackermann function:
    15 
    15 
    16   *}
    16   *}
    17 
    17 
    18 ML {* 
    18 ML{*fun ackermann (0, n) = n + 1
    19 fun ackermann (0, n) = n + 1
       
    20   | ackermann (m, 0) = ackermann (m - 1, 1)
    19   | ackermann (m, 0) = ackermann (m - 1, 1)
    21   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))
    20   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
    22 *}
       
    23 
    21 
    24 text {*
    22 text {*
    25 
    23 
    26   Now the call 
    24   Now the call 
    27 
    25