1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 15:57:34 2004 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Feb 19 16:44:21 2004 +0100
     1.3 @@ -370,10 +370,14 @@
     1.4    by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
     1.5      UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
     1.6  
     1.7 +lemma (in UP_cring) UP_ring:  (* preliminary *)
     1.8 +  "ring P"
     1.9 +  by (auto intro: ring.intro cring.axioms UP_cring)
    1.10 +
    1.11  lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
    1.12    "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
    1.13    by (rule abelian_group.a_inv_closed
    1.14 -    [OF cring.is_abelian_group [OF UP_cring]])
    1.15 +    [OF ring.is_abelian_group [OF UP_ring]])
    1.16  
    1.17  lemma (in UP_cring) coeff_a_inv [simp]:
    1.18    assumes R: "p \<in> carrier P"
    1.19 @@ -384,7 +388,7 @@
    1.20      by algebra
    1.21    also from R have "... =  \<ominus> (coeff P p n)"
    1.22      by (simp del: coeff_add add: coeff_add [THEN sym]
    1.23 -      abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
    1.24 +      abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
    1.25    finally show ?thesis .
    1.26  qed
    1.27  
    1.28 @@ -409,11 +413,11 @@
    1.29  
    1.30  lemma (in UP_cring) UP_abelian_monoid:
    1.31    "abelian_monoid P"
    1.32 -  by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
    1.33 +  by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
    1.34  
    1.35  lemma (in UP_cring) UP_abelian_group:
    1.36    "abelian_group P"
    1.37 -  by (fast intro!: cring.is_abelian_group UP_cring)
    1.38 +  by (fast intro!: ring.is_abelian_group UP_ring)
    1.39  
    1.40  lemmas (in UP_cring) UP_r_one [simp] =
    1.41    monoid.r_one [OF UP_monoid]
    1.42 @@ -521,19 +525,19 @@
    1.43    abelian_group.r_neg1 [OF UP_abelian_group]
    1.44  
    1.45  lemmas (in UP_cring) UP_r_distr =
    1.46 -  cring.r_distr [OF UP_cring]
    1.47 +  ring.r_distr [OF UP_ring]
    1.48  
    1.49  lemmas (in UP_cring) UP_l_null [simp] =
    1.50 -  cring.l_null [OF UP_cring]
    1.51 +  ring.l_null [OF UP_ring]
    1.52  
    1.53  lemmas (in UP_cring) UP_r_null [simp] =
    1.54 -  cring.r_null [OF UP_cring]
    1.55 +  ring.r_null [OF UP_ring]
    1.56  
    1.57  lemmas (in UP_cring) UP_l_minus =
    1.58 -  cring.l_minus [OF UP_cring]
    1.59 +  ring.l_minus [OF UP_ring]
    1.60  
    1.61  lemmas (in UP_cring) UP_r_minus =
    1.62 -  cring.r_minus [OF UP_cring]
    1.63 +  ring.r_minus [OF UP_ring]
    1.64  
    1.65  lemmas (in UP_cring) UP_finsum_ldistr =
    1.66    cring.finsum_ldistr [OF UP_cring]