1.1 --- a/src/HOL/Set.thy	Tue Mar 11 15:04:24 2003 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Mar 11 15:19:27 2003 +0100
     1.3 @@ -77,8 +77,10 @@
     1.4    "{x. P}"      == "Collect (%x. P)"
     1.5    "UN x y. B"   == "UN x. UN y. B"
     1.6    "UN x. B"     == "UNION UNIV (%x. B)"
     1.7 +  "UN x. B"     == "UN x:UNIV. B"
     1.8    "INT x y. B"  == "INT x. INT y. B"
     1.9    "INT x. B"    == "INTER UNIV (%x. B)"
    1.10 +  "INT x. B"    == "INT x:UNIV. B"
    1.11    "UN x:A. B"   == "UNION A (%x. B)"
    1.12    "INT x:A. B"  == "INTER A (%x. B)"
    1.13    "ALL x:A. P"  == "Ball A (%x. P)"
    1.14 @@ -157,7 +159,8 @@
    1.15      let val (x,t) = atomic_abs_tr' abs
    1.16      in Syntax.const syn $ x $ A $ t end
    1.17  in
    1.18 -[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
    1.19 +[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
    1.20 + ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
    1.21  end
    1.22  *}
    1.23