--- a/CookBook/Recipes/TimeLimit.thy Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy Wed Jan 14 16:46:07 2009 +0000
@@ -11,7 +11,7 @@
{\bf Solution:} This can be achieved using the function
@{ML timeLimit in TimeLimit}.\smallskip
- Assume the following infamous function:
+ Assume you defined the Ackermann function:
*}
@@ -27,7 +27,7 @@
@{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
- takes a bit of time to finish. To avoid this, the call can be encapsulated
+ takes a bit of time before it finishes. To avoid this, the call can be encapsulated
in a time limit of five seconds. For this you have to write:
@{ML_response [display]