diff -r c5c47703f763 -r dc677b35e54f src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 15:57:34 2004 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 16:44:21 2004 +0100
@@ -370,10 +370,14 @@
   by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
     UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
 
+lemma (in UP_cring) UP_ring:  (* preliminary *)
+  "ring P"
+  by (auto intro: ring.intro cring.axioms UP_cring)
+
 lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
   "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
   by (rule abelian_group.a_inv_closed
-    [OF cring.is_abelian_group [OF UP_cring]])
+    [OF ring.is_abelian_group [OF UP_ring]])
 
 lemma (in UP_cring) coeff_a_inv [simp]:
   assumes R: "p \<in> carrier P"
@@ -384,7 +388,7 @@
     by algebra
   also from R have "... =  \<ominus> (coeff P p n)"
     by (simp del: coeff_add add: coeff_add [THEN sym]
-      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
+      abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
   finally show ?thesis .
 qed
 
@@ -409,11 +413,11 @@
 
 lemma (in UP_cring) UP_abelian_monoid:
   "abelian_monoid P"
-  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
+  by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
 
 lemma (in UP_cring) UP_abelian_group:
   "abelian_group P"
-  by (fast intro!: cring.is_abelian_group UP_cring)
+  by (fast intro!: ring.is_abelian_group UP_ring)
 
 lemmas (in UP_cring) UP_r_one [simp] =
   monoid.r_one [OF UP_monoid]
@@ -521,19 +525,19 @@
   abelian_group.r_neg1 [OF UP_abelian_group]
 
 lemmas (in UP_cring) UP_r_distr =
-  cring.r_distr [OF UP_cring]
+  ring.r_distr [OF UP_ring]
 
 lemmas (in UP_cring) UP_l_null [simp] =
-  cring.l_null [OF UP_cring]
+  ring.l_null [OF UP_ring]
 
 lemmas (in UP_cring) UP_r_null [simp] =
-  cring.r_null [OF UP_cring]
+  ring.r_null [OF UP_ring]
 
 lemmas (in UP_cring) UP_l_minus =
-  cring.l_minus [OF UP_cring]
+  ring.l_minus [OF UP_ring]
 
 lemmas (in UP_cring) UP_r_minus =
-  cring.r_minus [OF UP_cring]
+  ring.r_minus [OF UP_ring]
 
 lemmas (in UP_cring) UP_finsum_ldistr =
   cring.finsum_ldistr [OF UP_cring]