--- a/src/HOL/Set.thy Thu Sep 28 14:41:48 2000 +0200
+++ b/src/HOL/Set.thy Thu Sep 28 14:42:21 2000 +0200
@@ -56,9 +56,8 @@
(* Big Intersection / Union *)
- "@INTER1" :: [pttrns, 'b set] => 'b set ("(3INT _./ _)" 10)
- "@UNION1" :: [pttrns, 'b set] => 'b set ("(3UN _./ _)" 10)
-
+ "@INTER1" :: [pttrns, 'b set] => 'b set ("(3INT _./ _)" 10)
+ "@UNION1" :: [pttrns, 'b set] => 'b set ("(3UN _./ _)" 10)
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3INT _:_./ _)" 10)
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10)
@@ -102,10 +101,8 @@
"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)
+ "@UNION1" :: [pttrns, 'b set] => 'b set ("(3\\<Union>_./ _)" 10)
+ "@INTER1" :: [pttrns, '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)