--- a/CookBook/Recipes/TimeLimit.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -1,41 +1,54 @@
 theory TimeLimit
-imports Base
+imports "../Base"
 begin
 
 section {* Restricting the Runtime of a Function *} 
 
-
 text {*
   {\bf Problem:}
-  Your tool should run only a specified amount of seconds.\smallskip
+  Your tool should run only a specified amount of time.\smallskip
 
-  {\bf Solution:} This can be achieved using time limits.\smallskip
+  {\bf Solution:} This can be achieved using the function 
+  @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume the following function should run only five seconds:
+  Assume the following well-known function:
 
   *}
 
-ML {*
+ML {* 
 fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))
 *}
 
-ML {* ackermann (3, 12) *}
+text {*
+
+  Now the call 
+
+  @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
 
-(* takes more than 10 seconds *)
+  takes a bit long. To avoid this, the call can be encapsulated 
+  in a time limit of five seconds. For this you have to write:
+
+@{ML_response [display]
+"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TimeOut => ~1"
+"~1"}
 
-text {*
-  The call can be encapsulated in a time limit of five seconds as follows:
-  *}
+  where @{ML_text TimeOut} is the exception raised when the time limit
+  is reached.
+
+  Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML, 
+  because PolyML has a rich infrastructure for multithreading programming on 
+  which @{ML "timeLimit" in TimeLimit} relies.
 
-ML {* 
-TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 
-  handle TimeOut => ~1
+\begin{readmore}
+   The function @{ML "timeLimit" in TimeLimit} is defined in the structure
+  @{ML_struct TimeLimit} which can be found in the file 
+  @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
+\end{readmore}
+
+ 
 *}
 
-text {*
-  The function "TimeLimit.timeLimit" has type "???" and is defined in
-  TODO: refer to code *}
-
 end
\ No newline at end of file