src/HOL/Library/Function_Algebras.thy
changeset 60500 903bb1495239
parent 59815 cce82e360c2f
child 60562 24af00b010cf
     1.1 --- a/src/HOL/Library/Function_Algebras.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Function_Algebras.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     1.5  *)
     1.6  
     1.7 -section {* Pointwise instantiation of functions to algebra type classes *}
     1.8 +section \<open>Pointwise instantiation of functions to algebra type classes\<close>
     1.9  
    1.10  theory Function_Algebras
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text {* Pointwise operations *}
    1.15 +text \<open>Pointwise operations\<close>
    1.16  
    1.17  instantiation "fun" :: (type, plus) plus
    1.18  begin
    1.19 @@ -59,7 +59,7 @@
    1.20    by (simp add: one_fun_def)
    1.21  
    1.22  
    1.23 -text {* Additive structures *}
    1.24 +text \<open>Additive structures\<close>
    1.25  
    1.26  instance "fun" :: (type, semigroup_add) semigroup_add
    1.27    by default (simp add: fun_eq_iff add.assoc)
    1.28 @@ -89,7 +89,7 @@
    1.29    by default simp_all
    1.30  
    1.31  
    1.32 -text {* Multiplicative structures *}
    1.33 +text \<open>Multiplicative structures\<close>
    1.34  
    1.35  instance "fun" :: (type, semigroup_mult) semigroup_mult
    1.36    by default (simp add: fun_eq_iff mult.assoc)
    1.37 @@ -104,7 +104,7 @@
    1.38    by default simp
    1.39  
    1.40  
    1.41 -text {* Misc *}
    1.42 +text \<open>Misc\<close>
    1.43  
    1.44  instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
    1.45  
    1.46 @@ -115,7 +115,7 @@
    1.47    by default (simp add: fun_eq_iff)
    1.48  
    1.49  
    1.50 -text {* Ring structures *}
    1.51 +text \<open>Ring structures\<close>
    1.52  
    1.53  instance "fun" :: (type, semiring) semiring
    1.54    by default (simp_all add: fun_eq_iff algebra_simps)
    1.55 @@ -176,7 +176,7 @@
    1.56  instance "fun" :: (type, ring_char_0) ring_char_0 ..
    1.57  
    1.58  
    1.59 -text {* Ordered structures *}
    1.60 +text \<open>Ordered structures\<close>
    1.61  
    1.62  instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
    1.63    by default (auto simp add: le_fun_def intro: add_left_mono)