1.1 --- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -155,27 +155,32 @@
     1.4  
     1.5  text {* The quotient of a cring is also commutative *}
     1.6  lemma (in ideal) quotient_is_cring:
     1.7 -  includes cring
     1.8 +  assumes "cring R"
     1.9    shows "cring (R Quot I)"
    1.10 -apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
    1.11 +proof -
    1.12 +  interpret cring [R] by fact
    1.13 +  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
    1.14    apply (rule quotient_is_ring)
    1.15   apply (rule ring.axioms[OF quotient_is_ring])
    1.16  apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
    1.17  apply clarify
    1.18  apply (simp add: rcoset_mult_add m_comm)
    1.19  done
    1.20 +qed
    1.21  
    1.22  text {* Cosets as a ring homomorphism on crings *}
    1.23  lemma (in ideal) rcos_ring_hom_cring:
    1.24 -  includes cring
    1.25 +  assumes "cring R"
    1.26    shows "ring_hom_cring R (R Quot I) (op +> I)"
    1.27 -apply (rule ring_hom_cringI)
    1.28 +proof -
    1.29 +  interpret cring [R] by fact
    1.30 +  show ?thesis apply (rule ring_hom_cringI)
    1.31    apply (rule rcos_ring_hom_ring)
    1.32   apply (rule R.is_cring)
    1.33  apply (rule quotient_is_cring)
    1.34  apply (rule R.is_cring)
    1.35  done
    1.36 -
    1.37 +qed
    1.38  
    1.39  subsection {* Factorization over Prime Ideals *}
    1.40  
    1.41 @@ -236,9 +241,11 @@
    1.42          The proof follows ``W. Adkins, S. Weintraub: Algebra --
    1.43          An Approach via Module Theory'' *}
    1.44  lemma (in maximalideal) quotient_is_field:
    1.45 -  includes cring
    1.46 +  assumes "cring R"
    1.47    shows "field (R Quot I)"
    1.48 -apply (intro cring.cring_fieldI2)
    1.49 +proof -
    1.50 +  interpret cring [R] by fact
    1.51 +  show ?thesis apply (intro cring.cring_fieldI2)
    1.52    apply (rule quotient_is_cring, rule is_cring)
    1.53   defer 1
    1.54   apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
    1.55 @@ -338,5 +345,6 @@
    1.56    from rcarr and this[symmetric]
    1.57    show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
    1.58  qed
    1.59 +qed
    1.60  
    1.61  end