100 "op Un" :: ['a set, 'a set] => 'a set (infixl "\\<union>" 65) |
100 "op Un" :: ['a set, 'a set] => 'a set (infixl "\\<union>" 65) |
101 "op :" :: ['a, 'a set] => bool ("op \\<in>") |
101 "op :" :: ['a, 'a set] => bool ("op \\<in>") |
102 "op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50) |
102 "op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50) |
103 "op ~:" :: ['a, 'a set] => bool ("op \\<notin>") |
103 "op ~:" :: ['a, 'a set] => bool ("op \\<notin>") |
104 "op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50) |
104 "op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50) |
105 "UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10) |
105 "UN " :: [idts, bool] => bool ("(3\\<Union>_./ _)" 10) |
106 "INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10) |
106 "INT " :: [idts, bool] => bool ("(3\\<Inter>_./ _)" 10) |
107 "@UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union> _./ _)" 10) |
107 "@UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union>_./ _)" 10) |
108 "@INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter> _./ _)" 10) |
108 "@INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter>_./ _)" 10) |
109 "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10) |
109 "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union>_\\<in>_./ _)" 10) |
110 "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10) |
110 "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter>_\\<in>_./ _)" 10) |
111 Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90) |
111 Union :: (('a set) set) => 'a set ("\\<Union>_" [90] 90) |
112 Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90) |
112 Inter :: (('a set) set) => 'a set ("\\<Inter>_" [90] 90) |
113 "_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10) |
113 "_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10) |
114 "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10) |
114 "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10) |
115 |
115 |
116 translations |
116 translations |
117 "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool" |
117 "op \\<subseteq>" => "op <= :: [_ set, _ set] => bool" |
118 "op \\<subset>" => "op < :: [_ set, _ set] => bool" |
118 "op \\<subset>" => "op < :: [_ set, _ set] => bool" |
119 |
119 |