106 Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) |
106 Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) |
107 Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) |
107 Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) |
108 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
108 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
109 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
109 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
110 |
110 |
|
111 syntax (HTML output) |
|
112 "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>") |
|
113 "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50) |
|
114 "_setless" :: "'a set => 'a set => bool" ("op \<subset>") |
|
115 "_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50) |
|
116 "op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70) |
|
117 "op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65) |
|
118 "op :" :: "'a => 'a set => bool" ("op \<in>") |
|
119 "op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50) |
|
120 "op ~:" :: "'a => 'a set => bool" ("op \<notin>") |
|
121 "op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50) |
|
122 "_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) |
|
123 "_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) |
|
124 |
111 syntax (input) |
125 syntax (input) |
112 "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) |
126 "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) |
113 "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) |
127 "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) |
114 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10) |
128 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10) |
115 "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10) |
129 "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10) |
117 syntax (xsymbols) |
131 syntax (xsymbols) |
118 "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10) |
132 "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10) |
119 "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10) |
133 "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10) |
120 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10) |
134 "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10) |
121 "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10) |
135 "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10) |
|
136 |
122 |
137 |
123 translations |
138 translations |
124 "op \<subseteq>" => "op <= :: _ set => _ set => bool" |
139 "op \<subseteq>" => "op <= :: _ set => _ set => bool" |
125 "op \<subset>" => "op < :: _ set => _ set => bool" |
140 "op \<subset>" => "op < :: _ set => _ set => bool" |
126 |
141 |