diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Johannes Hoelzl (TU Muenchen)
 *)
 
-section {* Indicator Function *}
+section \<open>Indicator Function\<close>
 
 theory Indicator_Function
 imports Complex_Main
@@ -88,7 +88,7 @@
   then have 
     "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
     "(indicator (\<Union> i. A i) x :: 'a) = 1"
-    using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
+    using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
   then show ?thesis
     by (rule_tac LIMSEQ_offset[of _ i]) simp
 qed (auto simp: indicator_def)
@@ -113,7 +113,7 @@
   then have 
     "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
     "(indicator (\<Inter>i. A i) x :: 'a) = 0"
-    using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
+    using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
   then show ?thesis
     by (rule_tac LIMSEQ_offset[of _ i]) simp
 qed (auto simp: indicator_def)