Undid eta change for UN/INT.
authornipkow
Tue, 25 Feb 2003 12:42:08 +0100
changeset 13826 e94aa103e12d
parent 13825 ef4c41e7956a
child 13827 c690cb885db4
Undid eta change for UN/INT.
src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 20 11:10:24 2003 +0100
+++ b/src/HOL/Set.thy	Tue Feb 25 12:42:08 2003 +0100
@@ -157,8 +157,7 @@
     let val (x,t) = atomic_abs_tr' abs
     in Syntax.const syn $ x $ A $ t end
 in
-[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
- ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
+[("Ball", btr' "_Ball"),("Bex", btr' "_Bex")]
 end
 *}