CookBook/Recipes/TimeLimit.thy
changeset 67 5fbeeac2901b
parent 63 83cea5dc6bac
child 68 e7519207c2b7
--- 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]