diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Product_plus.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Additive group operations on product types *}
+section \<open>Additive group operations on product types\<close>
 
 theory Product_plus
 imports Main
 begin
 
-subsection {* Operations *}
+subsection \<open>Operations\<close>
 
 instantiation prod :: (zero, zero) zero
 begin
@@ -78,7 +78,7 @@
 lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
   unfolding uminus_prod_def by simp
 
-subsection {* Class instances *}
+subsection \<open>Class instances\<close>
 
 instance prod :: (semigroup_add, semigroup_add) semigroup_add
   by default (simp add: prod_eq_iff add.assoc)