# HG changeset patch
# User lcp
# Date 797766181 -7200
# Node ID 9e3c9c84ab6fd09ab14bb2f6fd5fab5eae45cc66
# Parent  9458105037b6dbd4c3ee70c050ff3fa653245396
Redefined OUnion in a definitional manner

diff -r 9458105037b6 -r 9e3c9c84ab6f src/ZF/AC/OrdQuant.thy
--- a/src/ZF/AC/OrdQuant.thy	Thu Apr 13 11:41:34 1995 +0200
+++ b/src/ZF/AC/OrdQuant.thy	Thu Apr 13 11:43:01 1995 +0200
@@ -1,6 +1,6 @@
 (*  Title: 	ZF/AC/OrdQuant.thy
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Authors: 	Krzysztof Gr`abczewski and L C Paulson
 
 Quantifiers and union operator for ordinals. 
 *)
@@ -10,30 +10,29 @@
 consts
   
   (* Ordinal Quantifiers *)
-  Oall, Oex   :: "[i, i => o] => o"
-  (* General Union and Intersection *)
+  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)
-  "@Oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
-  "@Oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 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)"
-  "ALL x<a. P"  == "Oall(a, %x. P)"
-  "EX x<a. P"   == "Oex(a, %x. P)"
-
-rules
-  
-  OUnion_iff     "A : OUnion(a, %z. B(z)) <-> (EX x<a. A: B(x))"
 
 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)"
+  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