diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Recipes/Timing.thy
--- a/ProgTutorial/Recipes/Timing.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Recipes/Timing.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
 imports "../Appendix"
 begin
 
-section {* Measuring Time\label{rec:timing} *} 
+section \<open>Measuring Time\label{rec:timing}\<close> 
 
-text {*
+text \<open>
  {\bf Problem:}
   You want to measure the running time of a tactic or function.\smallskip
 
@@ -12,7 +12,7 @@
   @{ML start in Timing} and @{ML result in Timing}.\smallskip
 
   Suppose you defined the Ackermann function on the Isabelle level. 
-*}
+\<close>
 
 fun 
  ackermann:: "(nat \<times> nat) \<Rightarrow> nat"
@@ -21,24 +21,23 @@
   | "ackermann (m, 0) = ackermann (m - 1, 1)"
   | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
 
-text {* 
+text \<open>
   You can measure how long the simplifier takes to verify a datapoint
   of this function. The actual timing is done inside the
   wrapper function:
-*}
+\<close>
 
-ML %linenosgray{*fun timing_wrapper tac st =
+ML %linenosgray\<open>fun timing_wrapper tac st =
 let 
   val t_start = Timing.start ();
   val res = tac st;
   val t_end = Timing.result t_start;
 in
   (writeln (Timing.message t_end); res)
-end*}
+end\<close>
 
-text {*
-  Note that this function, in addition to a tactic, also takes a state @{text
-  "st"} as argument and applies this state to the tactic (Line 4). The reason is that
+text \<open>
+  Note that this function, in addition to a tactic, also takes a state \<open>st\<close> as argument and applies this state to the tactic (Line 4). The reason is that
   tactics are lazy functions and you need to force them to run, otherwise the
   timing will be meaningless. The simplifier tactic, amongst others,  can be 
   forced to run by just applying the state to it. But ``fully'' lazy tactics,
@@ -48,14 +47,14 @@
   The time between start and finish of the simplifier will be calculated 
   as the end time minus the start time.  An example of the
   wrapper is the proof
-*}
+\<close>
 
 lemma "ackermann (3, 4) = 125"
-apply(tactic {* 
-  timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1) *})
+apply(tactic \<open>
+  timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1)\<close>)
 done
 
-text {*
+text \<open>
   where it returns something on the scale of 3 seconds. We chose to return
   this information as a string, but the timing information is also accessible
   in number format.
@@ -65,7 +64,7 @@
   "Pure/General/timing.ML"} (for the PolyML compiler). Some more
   advanced functions are defined in @{ML_file "Pure/General/output.ML"}.
   \end{readmore}
-*}
+\<close>