src/HOL/Set.thy
changeset 13858 a077513c9a07
parent 13831 ab27b36aba99
child 13860 b681a3cb0beb
--- a/src/HOL/Set.thy	Tue Mar 11 15:04:24 2003 +0100
+++ b/src/HOL/Set.thy	Tue Mar 11 15:19:27 2003 +0100
@@ -77,8 +77,10 @@
   "{x. P}"      == "Collect (%x. P)"
   "UN x y. B"   == "UN x. UN y. B"
   "UN x. B"     == "UNION UNIV (%x. B)"
+  "UN x. B"     == "UN x:UNIV. B"
   "INT x y. B"  == "INT x. INT y. B"
   "INT x. B"    == "INTER UNIV (%x. B)"
+  "INT x. B"    == "INT x:UNIV. B"
   "UN x:A. B"   == "UNION A (%x. B)"
   "INT x:A. B"  == "INTER A (%x. B)"
   "ALL x:A. P"  == "Ball A (%x. P)"
@@ -157,7 +159,8 @@
     let val (x,t) = atomic_abs_tr' abs
     in Syntax.const syn $ x $ A $ t end
 in
-[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
+[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
+ ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
 end
 *}