src/HOL/Library/Quotient_Sum.thy
changeset 60500 903bb1495239
parent 58916 229765cc3414
child 62954 c5d0fdc260fa
--- a/src/HOL/Library/Quotient_Sum.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,13 +2,13 @@
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
-section {* Quotient infrastructure for the sum type *}
+section \<open>Quotient infrastructure for the sum type\<close>
 
 theory Quotient_Sum
 imports Main Quotient_Syntax
 begin
 
-subsection {* Rules for the Quotient package *}
+subsection \<open>Rules for the Quotient package\<close>
 
 lemma rel_sum_map1:
   "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"