src/HOL/Algebra/UnivPoly.thy
changeset 27714 27b4d7c01f8b
parent 27611 2c01c0bdb385
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Jul 30 19:03:33 2008 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jul 31 09:49:21 2008 +0200
     1.3 @@ -435,7 +435,7 @@
     1.4  
     1.5  lemma (in cring) cring:
     1.6    "cring R"
     1.7 -  by (fast intro: cring.intro prems)
     1.8 +  by unfold_locales
     1.9  
    1.10  lemma (in UP_cring) UP_algebra:
    1.11    "algebra R P"
    1.12 @@ -898,7 +898,7 @@
    1.13      and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
    1.14        b \<in> carrier R |] ==> a = zero R | b = zero R"
    1.15    shows "domain R"
    1.16 -  by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
    1.17 +  by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
    1.18      del: disjCI)
    1.19  
    1.20  lemma (in UP_domain) UP_one_not_zero:
    1.21 @@ -1251,7 +1251,7 @@
    1.22      and "h \<in> ring_hom R S"
    1.23    shows "ring_hom_cring R S h"
    1.24    by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
    1.25 -    cring.axioms prems)
    1.26 +    cring.axioms assms)
    1.27  
    1.28  lemma (in UP_pre_univ_prop) UP_hom_unique:
    1.29    assumes "ring_hom_cring P S Phi"