--- a/CookBook/Recipes/TimeLimit.thy Fri Jan 30 08:24:48 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy Fri Jan 30 16:58:31 2009 +0100
@@ -2,7 +2,7 @@
imports "../Base"
begin
-section {* Restricting the Runtime of a Function *}
+section {* Restricting the Runtime of a Function\label{rec:timeout} *}
text {*
{\bf Problem:}
@@ -30,7 +30,7 @@
@{ML_response [display,gray]
"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12)
- handle TimeOut => ~1"
+ handle TimeLimit.TimeOut => ~1"
"~1"}
where @{ML_text TimeOut} is the exception raised when the time limit