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