CookBook/Recipes/TimeLimit.thy
changeset 94 531e453c9d67
parent 72 7b8c4fe235aa
child 102 5e309df58557
--- 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