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.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)"
```