src/HOL/Library/Function_Algebras.thy

 (*  Title:      HOL/Library/Function_Algebras.thy
     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
 *)
 
-section {* Pointwise instantiation of functions to algebra type classes *}
+section \<open>Pointwise instantiation of functions to algebra type classes\<close>
 
 theory Function_Algebras
 imports Main
 begin
 
-text {* Pointwise operations *}
+text \<open>Pointwise operations\<close>
 
 instantiation "fun" :: (type, plus) plus
 begin
 
 definition "f + g = (\<lambda>x. f x + g x)"

 lemma one_fun_apply [simp]:
   "1 x = 1"
   by (simp add: one_fun_def)
 
 
-text {* Additive structures *}
+text \<open>Additive structures\<close>
 
 instance "fun" :: (type, semigroup_add) semigroup_add
   by default (simp add: fun_eq_iff add.assoc)
 
 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add

 
 instance "fun" :: (type, ab_group_add) ab_group_add
   by default simp_all
 
 
-text {* Multiplicative structures *}
+text \<open>Multiplicative structures\<close>
 
 instance "fun" :: (type, semigroup_mult) semigroup_mult
   by default (simp add: fun_eq_iff mult.assoc)
 
 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult

 
 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   by default simp
 
 
-text {* Misc *}
+text \<open>Misc\<close>
 
 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
 
 instance "fun" :: (type, mult_zero) mult_zero
   by default (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, zero_neq_one) zero_neq_one
   by default (simp add: fun_eq_iff)
 
 
-text {* Ring structures *}
+text \<open>Ring structures\<close>
 
 instance "fun" :: (type, semiring) semiring
   by default (simp_all add: fun_eq_iff algebra_simps)
 
 instance "fun" :: (type, comm_semiring) comm_semiring

 instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
 
 instance "fun" :: (type, ring_char_0) ring_char_0 ..
 
 
-text {* Ordered structures *}
+text \<open>Ordered structures\<close>
 
 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   by default (auto simp add: le_fun_def intro: add_left_mono)
 
 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..