src/HOL/Algebra/Ring.thy
 changeset 29237 e90d9d51106b parent 28823 dcbef866c9e2 child 35054 a5db9779b026
```     1.1 --- a/src/HOL/Algebra/Ring.thy	Tue Dec 16 15:09:37 2008 +0100
1.2 +++ b/src/HOL/Algebra/Ring.thy	Tue Dec 16 21:10:53 2008 +0100
1.3 @@ -1,6 +1,5 @@
1.4  (*
1.5    Title:     The algebraic hierarchy of rings
1.6 -  Id:        \$Id\$
1.7    Author:    Clemens Ballarin, started 9 December 1996
1.9  *)
1.10 @@ -187,7 +186,7 @@
1.11    assumes cg: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.12    shows "abelian_group G"
1.13  proof -
1.14 -  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
1.15 +  interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.16      by (rule cg)
1.17    show "abelian_group G" ..
1.18  qed
1.19 @@ -360,7 +359,7 @@
1.20
1.21  subsection {* Rings: Basic Definitions *}
1.22
1.23 -locale ring = abelian_group R + monoid R +
1.24 +locale ring = abelian_group R + monoid R for R (structure) +
1.25    assumes l_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.26        ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
1.27      and r_distr: "[| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
1.28 @@ -585,8 +584,8 @@
1.29    assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
1.30    shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
1.31  proof -
1.32 -  interpret ring [R] by fact
1.33 -  interpret cring [S] by fact
1.34 +  interpret ring R by fact
1.35 +  interpret cring S by fact
1.36  ML_val {* Algebra.print_structures @{context} *}
1.37    from RS show ?thesis by algebra
1.38  qed
1.39 @@ -597,7 +596,7 @@
1.40    assumes R: "a \<in> carrier R" "b \<in> carrier R"
1.41    shows "a \<ominus> (a \<ominus> b) = b"
1.42  proof -
1.43 -  interpret ring [R] by fact
1.44 +  interpret ring R by fact
1.45    from R show ?thesis by algebra
1.46  qed
1.47
1.48 @@ -771,7 +770,8 @@
1.49    shows "h \<in> ring_hom R S ==> h \<one> = \<one>\<^bsub>S\<^esub>"