src/ZF/AC/OrdQuant.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 1203 a39bec971684
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/AC/OrdQuant.thy
     2     ID:         $Id$
     3     Authors: 	Krzysztof Grabczewski and L C Paulson
     4 
     5 Quantifiers and union operator for ordinals. 
     6 *)
     7 
     8 OrdQuant = Ordinal +
     9 
    10 consts
    11   
    12   (* Ordinal Quantifiers *)
    13   oall, oex   :: [i, i => o] => o
    14 
    15   (* Ordinal Union *)
    16   OUnion      :: [i, i => i] => i
    17   
    18 syntax
    19   
    20   "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
    21   "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    22   "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    23 
    24 translations
    25   
    26   "ALL x<a. P"  == "oall(a, %x. P)"
    27   "EX x<a. P"   == "oex(a, %x. P)"
    28   "UN x<a. B"   == "OUnion(a, %x. B)"
    29 
    30 defs
    31   
    32   (* Ordinal Quantifiers *)
    33   oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
    34   oex_def       "oex(A, P) == EX x. x<A & P(x)"
    35 
    36   OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    37   
    38 end