# HG changeset patch
# User paulson
# Date 935659959 -7200
# Node ID 9e95b846ad42e3f3cadcf4d0e90e30489061d0de
# Parent  d0e16da40ea2786deaab6186e8c6e7cd08458e03
a little tidying; also FIXED BAD TYPE in INTER1, UNION1

diff -r d0e16da40ea2 -r 9e95b846ad42 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 25 20:49:02 1999 +0200
+++ b/src/HOL/Set.thy	Thu Aug 26 11:32:39 1999 +0200
@@ -56,8 +56,8 @@
 
   (* Big Intersection / Union *)
 
-  INTER1        :: [pttrns, 'a => 'b set] => 'b set   ("(3INT _./ _)" 10)
-  UNION1        :: [pttrns, 'a => '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)
@@ -104,8 +104,8 @@
   "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"     :: [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)