equal
deleted
inserted
replaced
20 |
20 |
21 text {* |
21 text {* |
22 |
22 |
23 Now the call |
23 Now the call |
24 |
24 |
25 @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"} |
25 @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"} |
26 |
26 |
27 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
27 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
28 in a time limit of five seconds. For this you have to write |
28 in a time limit of five seconds. For this you have to write |
29 |
29 |
30 @{ML_response_fake_both [display,gray] |
30 @{ML_response_fake_both [display,gray] |