src/ZF/ex/Ring.thy
 changeset 29223 e09c53289830 parent 28952 15a4b2cf8c34 child 41524 4d2f9a1c24c7
```     1.1 --- a/src/ZF/ex/Ring.thy	Wed Dec 10 17:19:25 2008 +0100
1.2 +++ b/src/ZF/ex/Ring.thy	Thu Dec 11 18:30:26 2008 +0100
1.3 @@ -45,7 +45,7 @@
1.4    minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
1.5    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
1.6
1.7 -locale abelian_monoid = struct G +
1.8 +locale abelian_monoid = fixes G (structure)
1.9    assumes a_comm_monoid:
1.10      "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
1.11
1.12 @@ -57,7 +57,7 @@
1.13    assumes a_comm_group:
1.14      "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
1.15
1.16 -locale ring = abelian_group R + monoid R +
1.17 +locale ring = abelian_group R + monoid R for R (structure) +
1.18    assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
1.19        \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
1.20      and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
1.21 @@ -262,7 +262,8 @@
1.22  lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
1.24
1.25 -locale ring_hom_cring = cring R + cring S + var h +
1.26 +locale ring_hom_cring = R: cring R + S: cring S
1.27 +  for R (structure) and S (structure) and h +
1.28    assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
1.29    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
1.30      and hom_mult [simp] = ring_hom_mult [OF homh]
```