# HG changeset patch
# User oheimb
# Date 949054922 -3600
# Node ID 5ef0b624aadb972337916f8c22e266fa647beb74
# Parent  b712b870a5d1b21cf14b96cf8c114c3c97cd67ad
beautified spacing for binders with symbols syntax, analogous to HOL.thy

diff -r b712b870a5d1 -r 5ef0b624aadb src/HOL/Set.thy
--- 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"