--- 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