# HG changeset patch
# User paulson
# Date 972307232 -7200
# Node ID 354e885b3e0a107e2fc97210cf7300ef08437689
# Parent  19753287b9df514e336cf1899d164fcae8854bd1
quantifiers now allowed in inductive defs

diff -r 19753287b9df -r 354e885b3e0a 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
diff -r 19753287b9df -r 354e885b3e0a src/HOL/UNITY/WFair.thy
--- 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