--- a/src/HOL/Finite_Set.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Finite_Set.thy Wed Apr 14 14:13:05 2004 +0200
@@ -746,6 +746,8 @@
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_:_. _" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0" ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+ "_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! *}
@@ -988,6 +990,9 @@
syntax (xsymbols)
"_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+syntax (HTML output)
+ "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+ ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
translations
"\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}