author | nipkow |
Tue, 25 Feb 2003 12:42:08 +0100 | |
changeset 13826 | e94aa103e12d |
parent 13825 | ef4c41e7956a |
child 13827 | c690cb885db4 |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- 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 *}