src/HOL/Algebra/QuotRing.thy
changeset 29242 e190bc2a5399
parent 29237 e90d9d51106b
child 35847 19f1f7066917
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 20:19:49 2008 +0100
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Fri Dec 19 11:09:09 2008 +0100
     1.3 @@ -175,9 +175,9 @@
     1.4    interpret cring R by fact
     1.5    show ?thesis apply (rule ring_hom_cringI)
     1.6    apply (rule rcos_ring_hom_ring)
     1.7 - apply (rule R.is_cring)
     1.8 + apply (rule is_cring)
     1.9  apply (rule quotient_is_cring)
    1.10 -apply (rule R.is_cring)
    1.11 +apply (rule is_cring)
    1.12  done
    1.13  qed
    1.14