src/HOL/Algebra/QuotRing.thy
changeset 29242 e190bc2a5399
parent 29237 e90d9d51106b
child 35847 19f1f7066917
--- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 20:19:49 2008 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Fri Dec 19 11:09:09 2008 +0100
@@ -175,9 +175,9 @@
   interpret cring R by fact
   show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
- apply (rule R.is_cring)
+ apply (rule is_cring)
 apply (rule quotient_is_cring)
-apply (rule R.is_cring)
+apply (rule is_cring)
 done
 qed