diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Progress.thy
--- a/src/HOL/UNITY/Comp/Progress.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,12 +5,12 @@
 David Meier's thesis
 *)
 
-section{*Progress Set Examples*}
+section\<open>Progress Set Examples\<close>
 
 theory Progress imports "../UNITY_Main" begin
 
-subsection {*The Composition of Two Single-Assignment Programs*}
-text{*Thesis Section 4.4.2*}
+subsection \<open>The Composition of Two Single-Assignment Programs\<close>
+text\<open>Thesis Section 4.4.2\<close>
 
 definition FF :: "int program" where
     "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
@@ -18,7 +18,7 @@
 definition GG :: "int program" where
     "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
 
-subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
+subsubsection \<open>Calculating @{term "wens_set FF (atLeast k)"}\<close>
 
 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
 by force
@@ -62,7 +62,7 @@
 apply (simp add: wens_single_finite_FF)
 done
 
-subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
+subsubsection \<open>Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}\<close>
 
 lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
 apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
@@ -86,7 +86,7 @@
 apply (rule leadsTo_UN [OF atLeast_leadsTo]) 
 done
 
-text{*Result (4.39): Applying the leadsTo-Join Theorem*}
+text\<open>Result (4.39): Applying the leadsTo-Join Theorem\<close>
 theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
  apply simp