Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/QuotRing.thy
changeset 35848 5443079512ea
parent 35847 19f1f7066917
child 35849 b5522b51cb1e 
--- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 16:51:37 2010 +0100
@@ -14,7 +14,7 @@
 definition
   rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
-  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)"
+  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))"
 
 
 text {* @{const "rcoset_mult"} fulfils the properties required by
@@ -91,7 +91,7 @@
 
 definition
   FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
-  where "FactRing R I \<equiv>
+  where "FactRing R I =
     \<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>"
isabelle