author | lcp |
Fri, 28 Jul 1995 11:02:22 +0200 | |
changeset 1203 | a39bec971684 |
parent 1200 | d4551b1a6da7 |
child 1401 | 0c439768f45c |
permissions | -rw-r--r-- |
1123 | 1 |
(* Title: ZF/AC/first.thy |
2 |
ID: $Id$ |
|
1203 | 3 |
Author: Krzysztof Grabczewski |
1123 | 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 |
||
1196 | 16 |
first_def "first(u, X, R) |
17 |
== u:X & (ALL v:X. v~=u --> <u,v> : R)" |
|
1200 | 18 |
end |