quantifiers now allowed in inductive defs

--- 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

--- a/src/HOL/UNITY/WFair.thy	Mon Oct 23 15:20:15 2000 +0200
+++ b/src/HOL/UNITY/WFair.thy	Mon Oct 23 15:20:32 2000 +0200
@@ -34,12 +34,7 @@
 
     Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
 
-    (*Encoding using powerset of the desired axiom
-       (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
-    *)
-    Union  "{(A,B) | A. A: S} : Pow (leads F) ==> (Union S, B) : leads F"
-
-  monos Pow_mono
+    Union  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
 
 
 constdefs