diff -r cf7f3465eaf1 -r 240563fbf41d src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/Sum.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -3,11 +3,11 @@
     Copyright   1993  University of Cambridge
 *)
 
-section{*Disjoint Sums*}
+section\<open>Disjoint Sums\<close>
 
 theory Sum imports Bool equalities begin
 
-text{*And the "Part" primitive for simultaneous recursive type definitions*}
+text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>
 
 definition sum :: "[i,i]=>i" (infixr "+" 65) where
      "A+B == {0}*A \<union> {1}*B"
@@ -25,7 +25,7 @@
 definition Part :: "[i,i=>i] => i" where
      "Part(A,h) == {x \<in> A. \<exists>z. x = h(z)}"
 
-subsection{*Rules for the @{term Part} Primitive*}
+subsection\<open>Rules for the @{term Part} Primitive\<close>
 
 lemma Part_iff:
     "a \<in> Part(A,h) \<longleftrightarrow> a \<in> A & (\<exists>y. a=h(y))"
@@ -51,7 +51,7 @@
 done
 
 
-subsection{*Rules for Disjoint Sums*}
+subsection\<open>Rules for Disjoint Sums\<close>
 
 lemmas sum_defs = sum_def Inl_def Inr_def case_def
 
@@ -125,7 +125,7 @@
 by (simp add: sum_def, blast)
 
 
-subsection{*The Eliminator: @{term case}*}
+subsection\<open>The Eliminator: @{term case}\<close>
 
 lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
 by (simp add: sum_defs)
@@ -159,7 +159,7 @@
 by auto
 
 
-subsection{*More Rules for @{term "Part(A,h)"}*}
+subsection\<open>More Rules for @{term "Part(A,h)"}\<close>
 
 lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
 by blast