src/HOL/Groups_Big.thy
changeset 60494 e726f88232d3
parent 60429 d3d1e185cd63
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Groups_Big.thy	Wed Jun 17 14:35:50 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Wed Jun 17 15:15:52 2015 +0100
     1.3 @@ -490,11 +490,11 @@
     1.4  written @{text"\<Sum>x\<in>A. e"}. *}
     1.5  
     1.6  syntax
     1.7 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
     1.8 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
     1.9  syntax (xsymbols)
    1.10 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.11 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    1.12  syntax (HTML output)
    1.13 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
    1.14 +  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    1.15  
    1.16  translations -- {* Beware of argument permutation! *}
    1.17    "SUM i:A. b" == "CONST setsum (%i. b) A"
    1.18 @@ -506,9 +506,9 @@
    1.19  syntax
    1.20    "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    1.21  syntax (xsymbols)
    1.22 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.23 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.24  syntax (HTML output)
    1.25 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.26 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    1.27  
    1.28  translations
    1.29    "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
    1.30 @@ -1054,11 +1054,11 @@
    1.31  end
    1.32  
    1.33  syntax
    1.34 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
    1.35 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
    1.36  syntax (xsymbols)
    1.37 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.38 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    1.39  syntax (HTML output)
    1.40 -  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
    1.41 +  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    1.42  
    1.43  translations -- {* Beware of argument permutation! *}
    1.44    "PROD i:A. b" == "CONST setprod (%i. b) A" 
    1.45 @@ -1068,11 +1068,11 @@
    1.46   @{text"\<Prod>x|P. e"}. *}
    1.47  
    1.48  syntax
    1.49 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
    1.50 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
    1.51  syntax (xsymbols)
    1.52 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.53 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.54  syntax (HTML output)
    1.55 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.56 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    1.57  
    1.58  translations
    1.59    "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"