src/HOL/Algebra/QuotRing.thy
changeset 23463 9953ff53cc64
parent 23350 50c5b0912a0c
child 27611 2c01c0bdb385
--- a/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -4,17 +4,17 @@
   Author:    Stephan Hohe
 *)
 
+header {* Quotient Rings *}
+
 theory QuotRing
 imports RingHom
 begin
 
-
-section {* Quotient Rings *}
-
 subsection {* Multiplication on Cosets *}
 
 constdefs (structure R)
-  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"   ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
+  rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
+    ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
   "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
 
 
@@ -171,8 +171,9 @@
   shows "ring_hom_cring R (R Quot I) (op +> I)"
 apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
- apply assumption
-apply (rule quotient_is_cring, assumption)
+ apply (rule R.is_cring)
+apply (rule quotient_is_cring)
+apply (rule R.is_cring)
 done