src/HOL/UNITY/ELT.thy

--- a/src/HOL/UNITY/ELT.thy	Mon Oct 23 15:20:15 2000 +0200
+++ b/src/HOL/UNITY/ELT.thy	Mon Oct 23 15:20:32 2000 +0200
@@ -37,9 +37,7 @@
 
     Trans  "[| (A,B) : elt CC F;  (B,C) : elt CC F |] ==> (A,C) : elt CC F"
 
-    Union  "{(A,B) | A. A: S} : Pow (elt CC F) ==> (Union S, B) : elt CC F"
-
-  monos Pow_mono
+    Union  "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F"
 
 
 constdefs