diff -r b98cd131e2b5 -r 5b5656a63bd6 src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/While_Combinator_Example.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -3,14 +3,14 @@
     Copyright   2000 TU Muenchen
 *)
 
-section {* An application of the While combinator *}
+section \<open>An application of the While combinator\<close>
 
 theory While_Combinator_Example
 imports "~~/src/HOL/Library/While_Combinator"
 begin
 
-text {* Computation of the @{term lfp} on finite sets via 
-  iteration. *}
+text \<open>Computation of the @{term lfp} on finite sets via 
+  iteration.\<close>
 
 theorem lfp_conv_while:
   "[| mono f; finite U; f U = U |] ==>
@@ -32,11 +32,11 @@
 done
 
 
-subsection {* Example *}
+subsection \<open>Example\<close>
 
-text{* Cannot use @{thm[source]set_eq_subset} because it leads to
+text\<open>Cannot use @{thm[source]set_eq_subset} because it leads to
 looping because the antisymmetry simproc turns the subset relationship
-back into equality. *}
+back into equality.\<close>
 
 theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
   P {0, 4, 2}"
@@ -52,7 +52,7 @@
       apply blast
      apply simp
     apply (simp add: aux set_eq_subset)
-    txt {* The fixpoint computation is performed purely by rewriting: *}
+    txt \<open>The fixpoint computation is performed purely by rewriting:\<close>
     apply (simp add: while_unfold aux seteq del: subset_empty)
     done
 qed