src/HOL/Algebra/Module.thy
changeset 61382 efac889fccbc
parent 58860 fee7cfa69c50
child 61565 352c73a689da
     1.1 --- a/src/HOL/Algebra/Module.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Module.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -7,9 +7,9 @@
     1.4  imports Ring
     1.5  begin
     1.6  
     1.7 -section {* Modules over an Abelian Group *}
     1.8 +section \<open>Modules over an Abelian Group\<close>
     1.9  
    1.10 -subsection {* Definitions *}
    1.11 +subsection \<open>Definitions\<close>
    1.12  
    1.13  record ('a, 'b) module = "'b ring" +
    1.14    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    1.15 @@ -103,7 +103,7 @@
    1.16      smult_l_distr smult_r_distr smult_assoc1)
    1.17  
    1.18  
    1.19 -subsection {* Basic Properties of Algebras *}
    1.20 +subsection \<open>Basic Properties of Algebras\<close>
    1.21  
    1.22  lemma (in algebra) smult_l_null [simp]:
    1.23    "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"