81 syntax |
81 syntax |
82 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10) |
82 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10) |
83 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10) |
83 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10) |
84 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10) |
84 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10) |
85 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10) |
85 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10) |
|
86 |
|
87 syntax_consts |
|
88 "_UNION_le" "_UNION_less" \<rightleftharpoons> Union and |
|
89 "_INTER_le" "_INTER_less" \<rightleftharpoons> Inter |
86 |
90 |
87 translations |
91 translations |
88 "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A" |
92 "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A" |
89 "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A" |
93 "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A" |
90 "\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A" |
94 "\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A" |
2003 "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
2007 "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) |
2004 "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
2008 "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) |
2005 "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
2009 "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) |
2006 "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) |
2010 "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) |
2007 |
2011 |
|
2012 syntax_consts |
|
2013 "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum |
|
2014 |
2008 translations |
2015 translations |
2009 "\<Sum>x=a..b. t" == "CONST sum (\<lambda>x. t) {a..b}" |
2016 "\<Sum>x=a..b. t" == "CONST sum (\<lambda>x. t) {a..b}" |
2010 "\<Sum>x=a..<b. t" == "CONST sum (\<lambda>x. t) {a..<b}" |
2017 "\<Sum>x=a..<b. t" == "CONST sum (\<lambda>x. t) {a..<b}" |
2011 "\<Sum>i\<le>n. t" == "CONST sum (\<lambda>i. t) {..n}" |
2018 "\<Sum>i\<le>n. t" == "CONST sum (\<lambda>i. t) {..n}" |
2012 "\<Sum>i<n. t" == "CONST sum (\<lambda>i. t) {..<n}" |
2019 "\<Sum>i<n. t" == "CONST sum (\<lambda>i. t) {..<n}" |
2693 "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) |
2700 "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10) |
2694 "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) |
2701 "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10) |
2695 "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) |
2702 "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10) |
2696 "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) |
2703 "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10) |
2697 |
2704 |
|
2705 syntax_consts |
|
2706 "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod |
|
2707 |
2698 translations |
2708 translations |
2699 "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}" |
2709 "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}" |
2700 "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}" |
2710 "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}" |
2701 "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}" |
2711 "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}" |
2702 "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}" |
2712 "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}" |