--- a/src/HOL/Set.thy Thu Jan 27 15:30:10 2000 +0100
+++ b/src/HOL/Set.thy Fri Jan 28 11:22:02 2000 +0100
@@ -102,16 +102,16 @@
"op :" :: ['a, 'a set] => bool ("(_/ \\<in> _)" [50, 51] 50)
"op ~:" :: ['a, 'a set] => bool ("op \\<notin>")
"op ~:" :: ['a, 'a set] => bool ("(_/ \\<notin> _)" [50, 51] 50)
- "UN " :: [idts, bool] => bool ("(3\\<Union> _./ _)" 10)
- "INT " :: [idts, bool] => bool ("(3\\<Inter> _./ _)" 10)
- "@UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union> _./ _)" 10)
- "@INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter> _./ _)" 10)
- "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union> _\\<in>_./ _)" 10)
- "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10)
- Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90)
- Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90)
- "_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
- "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
+ "UN " :: [idts, bool] => bool ("(3\\<Union>_./ _)" 10)
+ "INT " :: [idts, bool] => bool ("(3\\<Inter>_./ _)" 10)
+ "@UNION1" :: [pttrn, 'b set] => 'b set ("(3\\<Union>_./ _)" 10)
+ "@INTER1" :: [pttrn, 'b set] => 'b set ("(3\\<Inter>_./ _)" 10)
+ "@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Union>_\\<in>_./ _)" 10)
+ "@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter>_\\<in>_./ _)" 10)
+ Union :: (('a set) set) => 'a set ("\\<Union>_" [90] 90)
+ Inter :: (('a set) set) => 'a set ("\\<Inter>_" [90] 90)
+ "_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall>_\\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists>_\\<in>_./ _)" [0, 0, 10] 10)
translations
"op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"