src/HOL/Algebra/QuotRing.thy
changeset 29237 e90d9d51106b
parent 27717 21bbd410ba04
child 29242 e190bc2a5399
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Dec 16 15:09:37 2008 +0100
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Dec 16 21:10:53 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5    Title:     HOL/Algebra/QuotRing.thy
     1.6 -  Id:        $Id$
     1.7    Author:    Stephan Hohe
     1.8  *)
     1.9  
    1.10 @@ -158,7 +157,7 @@
    1.11    assumes "cring R"
    1.12    shows "cring (R Quot I)"
    1.13  proof -
    1.14 -  interpret cring [R] by fact
    1.15 +  interpret cring R by fact
    1.16    show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
    1.17    apply (rule quotient_is_ring)
    1.18   apply (rule ring.axioms[OF quotient_is_ring])
    1.19 @@ -173,7 +172,7 @@
    1.20    assumes "cring R"
    1.21    shows "ring_hom_cring R (R Quot I) (op +> I)"
    1.22  proof -
    1.23 -  interpret cring [R] by fact
    1.24 +  interpret cring R by fact
    1.25    show ?thesis apply (rule ring_hom_cringI)
    1.26    apply (rule rcos_ring_hom_ring)
    1.27   apply (rule R.is_cring)
    1.28 @@ -244,7 +243,7 @@
    1.29    assumes "cring R"
    1.30    shows "field (R Quot I)"
    1.31  proof -
    1.32 -  interpret cring [R] by fact
    1.33 +  interpret cring R by fact
    1.34    show ?thesis apply (intro cring.cring_fieldI2)
    1.35    apply (rule quotient_is_cring, rule is_cring)
    1.36   defer 1