src/HOL/Finite_Set.thy
changeset 14565 c6dc17aab88a
parent 14504 7a3d80e276d4
child 14661 9ead82084de8
     1.1 --- a/src/HOL/Finite_Set.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -746,6 +746,8 @@
     1.4    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_:_. _" [0, 51, 10] 10)
     1.5  syntax (xsymbols)
     1.6    "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
     1.7 +syntax (HTML output)
     1.8 +  "_setsum" :: "idt => 'a set => 'b => 'b::plus_ac0"    ("\<Sum>_\<in>_. _" [0, 51, 10] 10)
     1.9  translations
    1.10    "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
    1.11  
    1.12 @@ -988,6 +990,9 @@
    1.13  syntax (xsymbols)
    1.14    "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
    1.15                  ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
    1.16 +syntax (HTML output)
    1.17 +  "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
    1.18 +                ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
    1.19  translations
    1.20    "\<Prod>i:A. b" == "setprod (%i. b) A"  -- {* Beware of argument permutation! *}
    1.21