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