--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/OrdQuant.thy Fri Jan 03 15:01:55 1997 +0100
@@ -0,0 +1,38 @@
+(* Title: ZF/AC/OrdQuant.thy
+ ID: $Id$
+ Authors: Krzysztof Grabczewski and L C Paulson
+
+Quantifiers and union operator for ordinals.
+*)
+
+OrdQuant = Ordinal +
+
+consts
+
+ (* Ordinal Quantifiers *)
+ oall, oex :: [i, i => o] => o
+
+ (* Ordinal Union *)
+ OUnion :: [i, i => i] => i
+
+syntax
+
+ "@oall" :: [idt, i, o] => o ("(3ALL _<_./ _)" 10)
+ "@oex" :: [idt, i, o] => o ("(3EX _<_./ _)" 10)
+ "@OUNION" :: [idt, i, i] => i ("(3UN _<_./ _)" 10)
+
+translations
+
+ "ALL x<a. P" == "oall(a, %x. P)"
+ "EX x<a. P" == "oex(a, %x. P)"
+ "UN x<a. B" == "OUnion(a, %x. B)"
+
+defs
+
+ (* Ordinal Quantifiers *)
+ oall_def "oall(A, P) == ALL x. x<A --> P(x)"
+ oex_def "oex(A, P) == EX x. x<A & P(x)"
+
+ OUnion_def "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
+
+end