src/HOL/Algebra/QuotRing.thy
changeset 27611 2c01c0bdb385
parent 23463 9953ff53cc64
child 27717 21bbd410ba04
--- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:02:10 2008 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 15 16:50:09 2008 +0200
@@ -155,27 +155,32 @@
 
 text {* The quotient of a cring is also commutative *}
 lemma (in ideal) quotient_is_cring:
-  includes cring
+  assumes "cring R"
   shows "cring (R Quot I)"
-apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro)
   apply (rule quotient_is_ring)
  apply (rule ring.axioms[OF quotient_is_ring])
 apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric])
 apply clarify
 apply (simp add: rcoset_mult_add m_comm)
 done
+qed
 
 text {* Cosets as a ring homomorphism on crings *}
 lemma (in ideal) rcos_ring_hom_cring:
-  includes cring
+  assumes "cring R"
   shows "ring_hom_cring R (R Quot I) (op +> I)"
-apply (rule ring_hom_cringI)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
  apply (rule R.is_cring)
 apply (rule quotient_is_cring)
 apply (rule R.is_cring)
 done
-
+qed
 
 subsection {* Factorization over Prime Ideals *}
 
@@ -236,9 +241,11 @@
         The proof follows ``W. Adkins, S. Weintraub: Algebra --
         An Approach via Module Theory'' *}
 lemma (in maximalideal) quotient_is_field:
-  includes cring
+  assumes "cring R"
   shows "field (R Quot I)"
-apply (intro cring.cring_fieldI2)
+proof -
+  interpret cring [R] by fact
+  show ?thesis apply (intro cring.cring_fieldI2)
   apply (rule quotient_is_cring, rule is_cring)
  defer 1
  apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
@@ -338,5 +345,6 @@
   from rcarr and this[symmetric]
   show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
 qed
+qed
 
 end