src/HOL/Algebra/Ring.thy
changeset 27714 27b4d7c01f8b
parent 27699 489e3f33af0e
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/Ring.thy	Wed Jul 30 19:03:33 2008 +0200
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Thu Jul 31 09:49:21 2008 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4      and a_comm:
     1.5        "!!x y. [| x \<in> carrier R; y \<in> carrier R |] ==> x \<oplus> y = y \<oplus> x"
     1.6    shows "abelian_monoid R"
     1.7 -  by (auto intro!: abelian_monoid.intro comm_monoidI intro: prems)
     1.8 +  by (auto intro!: abelian_monoid.intro comm_monoidI intro: assms)
     1.9  
    1.10  lemma abelian_groupI:
    1.11    fixes R (structure)
    1.12 @@ -70,7 +70,7 @@
    1.13    shows "abelian_group R"
    1.14    by (auto intro!: abelian_group.intro abelian_monoidI
    1.15        abelian_group_axioms.intro comm_monoidI comm_groupI
    1.16 -    intro: prems)
    1.17 +    intro: assms)
    1.18  
    1.19  lemma (in abelian_monoid) a_monoid:
    1.20    "monoid (| carrier = carrier G, mult = add G, one = zero G |)"
    1.21 @@ -374,7 +374,7 @@
    1.22        ==> z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y"
    1.23    shows "ring R"
    1.24    by (auto intro: ring.intro
    1.25 -    abelian_group.axioms ring_axioms.intro prems)
    1.26 +    abelian_group.axioms ring_axioms.intro assms)
    1.27  
    1.28  lemma (in ring) is_abelian_group:
    1.29    "abelian_group R"
    1.30 @@ -416,7 +416,7 @@
    1.31      finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
    1.32    qed (rule l_distr)
    1.33  qed (auto intro: cring.intro
    1.34 -  abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
    1.35 +  abelian_group.axioms comm_monoid.axioms ring_axioms.intro assms)
    1.36  
    1.37  (*
    1.38  lemma (in cring) is_comm_monoid:
    1.39 @@ -731,7 +731,7 @@
    1.40        h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y"
    1.41      and hom_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
    1.42    shows "h \<in> ring_hom R S"
    1.43 -  by (auto simp add: ring_hom_def prems Pi_def)
    1.44 +  by (auto simp add: ring_hom_def assms Pi_def)
    1.45  
    1.46  lemma ring_hom_closed:
    1.47    "[| h \<in> ring_hom R S; x \<in> carrier R |] ==> h x \<in> carrier S"