diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -16,12 +16,12 @@
 
 text {* Derived operations. *}
 
-constdefs
-  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
+constdefs (structure R)
+  a_inv :: "[_, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
   "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
 
   minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
 
 locale abelian_monoid = struct G +
   assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
@@ -183,10 +183,22 @@
 *}
 
 constdefs
-  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+  finsum :: "[_, 'a => 'b, 'a set] => 'b"
   "finsum G f A == finprod (| carrier = carrier G,
      mult = add G, one = zero G |) f A"
 
+syntax
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+syntax (xsymbols)
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+syntax (HTML output)
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+translations
+  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
+
 (*
   lemmas (in abelian_monoid) finsum_empty [simp] =
     comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
@@ -214,7 +226,7 @@
     folded finsum_def, simplified monoid_record_simps])
 
 lemma (in abelian_monoid) finsum_zero [simp]:
-  "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
+  "finite A ==> (\<Oplus>i: A. \<zero>) = \<zero>"
   by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])