src/HOL/Algebra/Module.thy
changeset 29237 e90d9d51106b
parent 28823 dcbef866c9e2
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/Module.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/Module.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Algebra/Module.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Clemens Ballarin, started 15 April 2003
     1.7      Copyright:  Clemens Ballarin
     1.8  *)
     1.9 @@ -14,7 +13,7 @@
    1.10  record ('a, 'b) module = "'b ring" +
    1.11    smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    1.12  
    1.13 -locale module = cring R + abelian_group M +
    1.14 +locale module = R: cring + M: abelian_group M for M (structure) +
    1.15    assumes smult_closed [simp, intro]:
    1.16        "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    1.17      and smult_l_distr:
    1.18 @@ -29,7 +28,7 @@
    1.19      and smult_one [simp]:
    1.20        "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    1.21  
    1.22 -locale algebra = module R M + cring M +
    1.23 +locale algebra = module + cring M +
    1.24    assumes smult_assoc2:
    1.25        "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.26        (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"