src/ZF/AC/first.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/AC/first.thy
lcp@1123
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Krzysztof Grabczewski
lcp@1123
     4
lcp@1123
     5
Theory helpful in proofs using first element of a well ordered set
lcp@1123
     6
*)
lcp@1123
     7
lcp@1123
     8
first = Order +
lcp@1123
     9
lcp@1123
    10
consts
lcp@1123
    11
clasohm@1401
    12
  first                   :: [i, i, i] => o
lcp@1123
    13
lcp@1123
    14
defs
lcp@1123
    15
lcp@1196
    16
  first_def                "first(u, X, R) 
clasohm@1478
    17
                            == u:X & (ALL v:X. v~=u --> <u,v> : R)"
lcp@1200
    18
end