diff -r 5b9c6010897b -r 64c9540f2f84 CookBook/Recipes/TimeLimit.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 07 16:29:49 2009 +0100
@@ -0,0 +1,41 @@
+theory TimeLimit
+imports Base
+begin
+
+section {* Restricting the Runtime of a Function *} 
+
+
+text {*
+  {\bf Problem:}
+  Your tool should run only a specified amount of seconds.\smallskip
+
+  {\bf Solution:} This can be achieved using time limits.\smallskip
+
+  Assume the following function should run only five seconds:
+
+  *}
+
+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) *}
+
+(* takes more than 10 seconds *)
+
+text {*
+  The call can be encapsulated in a time limit of five seconds as follows:
+  *}
+
+ML {* 
+TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (3, 12) 
+  handle TimeOut => ~1
+*}
+
+text {*
+  The function "TimeLimit.timeLimit" has type "???" and is defined in
+  TODO: refer to code *}
+
+end
\ No newline at end of file