src/HOL/Algebra/QuotRing.thy
changeset 35848 5443079512ea
parent 35847 19f1f7066917
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 15:57:40 2010 +0100
     1.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 16:51:37 2010 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  definition
     1.5    rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     1.6      ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
     1.7 -  where "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b)"
     1.8 +  where "rcoset_mult R I A B = (\<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b))"
     1.9  
    1.10  
    1.11  text {* @{const "rcoset_mult"} fulfils the properties required by
    1.12 @@ -91,7 +91,7 @@
    1.13  
    1.14  definition
    1.15    FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
    1.16 -  where "FactRing R I \<equiv>
    1.17 +  where "FactRing R I =
    1.18      \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
    1.19  
    1.20