changeset 12114 | a8e860c86252 |
parent 11786 | 51ce34ef5113 |
child 12338 | de0f4a63baa5 |
--- a/src/HOL/Finite.thy Fri Nov 09 00:06:15 2001 +0100 +++ b/src/HOL/Finite.thy Fri Nov 09 00:09:47 2001 +0100 @@ -63,7 +63,7 @@ syntax "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_:_. _" [0, 51, 10] 10) -syntax (symbols) +syntax (xsymbols) "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\\<Sum>_\\<in>_. _" [0, 51, 10] 10) translations "\\<Sum>i:A. b" == "setsum (%i. b) A" (* Beware of argument permutation! *)