52 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
52 text{* A note of warning when using @{term"{..<n}"} on type @{typ |
53 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
53 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
54 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
54 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *} |
55 |
55 |
56 syntax |
56 syntax |
57 "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
57 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10) |
58 "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
58 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10) |
59 "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
59 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10) |
60 "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10) |
60 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10) |
61 |
61 |
62 syntax (xsymbols) |
62 syntax (xsymbols) |
63 "@UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) |
63 "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10) |
64 "@UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
64 "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10) |
65 "@INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
65 "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10) |
66 "@INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
66 "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10) |
67 |
67 |
68 syntax (latex output) |
68 syntax (latex output) |
69 "@UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10) |
69 "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10) |
70 "@UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10) |
70 "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10) |
71 "@INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10) |
71 "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10) |
72 "@INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10) |
72 "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10) |
73 |
73 |
74 translations |
74 translations |
75 "UN i<=n. A" == "UN i:{..n}. A" |
75 "UN i<=n. A" == "UN i:{..n}. A" |
76 "UN i<n. A" == "UN i:{..<n}. A" |
76 "UN i<n. A" == "UN i:{..<n}. A" |
77 "INT i<=n. A" == "INT i:{..n}. A" |
77 "INT i<=n. A" == "INT i:{..n}. A" |