--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,50 @@
+theory TimeLimit
+imports "../Base"
+begin
+
+section {* Restricting the Runtime of a Function\label{rec:timeout} *} 
+
+text {*
+  {\bf Problem:}
+  Your tool should run only a specified amount of time.\smallskip
+
+  {\bf Solution:} This can be achieved using the function 
+  @{ML timeLimit in TimeLimit}.\smallskip
+
+  Assume you defined the Ackermann function on the ML-level.
+*}
+
+ML{*fun ackermann (0, n) = n + 1
+  | ackermann (m, 0) = ackermann (m - 1, 1)
+  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
+
+text {*
+
+  Now the call 
+
+  @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
+
+  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_fake_both [display,gray]
+"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TimeLimit.TimeOut => ~1"
+"~1"}
+
+  where @{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 5.2.1
+  or later, because this version of PolyML has the infrastructure for multithreaded 
+  programming on which @{ML "timeLimit" in TimeLimit} relies.
+
+\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}
+
+ 
+*}
+end
\ No newline at end of file