# HG changeset patch
# User wenzelm
# Date 970144941 -7200
# Node ID 1b63e30437ee54d56773a5655f62e39c2d30e9af
# Parent  f9be78009930a3648a000571e19bb92af056a335
fixed \<Union>, \<Inter> syntax;

diff -r f9be78009930 -r 1b63e30437ee src/HOL/Set.thy
--- 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)