diff -r 62fb91f86908 -r 531e453c9d67 CookBook/Recipes/TimeLimit.thy --- 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