src/HOL/Library/Product_plus.thy
changeset 60500 903bb1495239
parent 59815 cce82e360c2f
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Product_plus.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Additive group operations on product types *}
     1.8 +section \<open>Additive group operations on product types\<close>
     1.9  
    1.10  theory Product_plus
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -subsection {* Operations *}
    1.15 +subsection \<open>Operations\<close>
    1.16  
    1.17  instantiation prod :: (zero, zero) zero
    1.18  begin
    1.19 @@ -78,7 +78,7 @@
    1.20  lemma uminus_Pair [simp, code]: "- (a, b) = (- a, - b)"
    1.21    unfolding uminus_prod_def by simp
    1.22  
    1.23 -subsection {* Class instances *}
    1.24 +subsection \<open>Class instances\<close>
    1.25  
    1.26  instance prod :: (semigroup_add, semigroup_add) semigroup_add
    1.27    by default (simp add: prod_eq_iff add.assoc)