src/HOL/Library/Groups_Big_Fun.thy
changeset 61955 e96292f32c3c
parent 61776 57bb7da5c867
child 63290 9ac558ab0906
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -233,12 +233,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 -syntax
     1.8 +syntax (ASCII)
     1.9    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
    1.10 -syntax (xsymbols)
    1.11 +syntax
    1.12    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
    1.13  translations
    1.14 -  "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
    1.15 +  "\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
    1.16  
    1.17  lemma Sum_any_left_distrib:
    1.18    fixes r :: "'a :: semiring_0"
    1.19 @@ -302,10 +302,10 @@
    1.20  
    1.21  end
    1.22  
    1.23 +syntax (ASCII)
    1.24 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
    1.25  syntax
    1.26 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
    1.27 -syntax (xsymbols)
    1.28 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
    1.29 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_. _)" [0, 10] 10)
    1.30  translations
    1.31    "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
    1.32