diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Recipes/TimeLimit.thy --- a/ProgTutorial/Recipes/TimeLimit.thy Tue May 14 16:59:53 2019 +0200 +++ b/ProgTutorial/Recipes/TimeLimit.thy Tue May 14 17:10:47 2019 +0200 @@ -2,8 +2,8 @@ imports "../Appendix" begin -section {* Restricting the Runtime of a Function\label{rec:timeout} *} -text {* +section \<open>Restricting the Runtime of a Function\label{rec:timeout}\<close> +text \<open> {\bf Problem:} Your tool should run only a specified amount of time.\smallskip @@ -11,13 +11,13 @@ using the function @{ML apply in Timeout}.\smallskip Assume you defined the Ackermann function on the ML-level. -*} +\<close> -ML %grayML{*fun ackermann (0, n) = n + 1 +ML %grayML\<open>fun ackermann (0, n) = n + 1 | ackermann (m, 0) = ackermann (m - 1, 1) - | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *} + | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))\<close> -text {* +text \<open> Now the call @@ -31,7 +31,7 @@ handle TIMEOUT => ~1" "~1"} - where @{text TimeOut} is the exception raised when the time limit + where \<open>TimeOut\<close> is the exception raised when the time limit is reached. Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1 @@ -45,5 +45,5 @@ \end{readmore} -*} +\<close> end