diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-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