| changeset 2469 | b50b8c0eec01 |
| parent 2468 | 428efffe8599 |
| child 2470 | 273580d5c040 |
| 2468:428efffe8599 | 2469:b50b8c0eec01 |
|---|---|
1 (* Title: ZF/AC/first.thy |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 Theory helpful in proofs using first element of a well ordered set |
|
6 *) |
|
7 |
|
8 first = Order + |
|
9 |
|
10 consts |
|
11 |
|
12 first :: [i, i, i] => o |
|
13 |
|
14 defs |
|
15 |
|
16 first_def "first(u, X, R) |
|
17 == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
|
18 end |