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
*)

+
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

```