author | lcp |
Tue, 29 Nov 1994 00:31:31 +0100 | |
changeset 753 | ec86863e87c8 |
parent 124 | 858ab9a9b047 |
child 1401 | 0c439768f45c |
permissions | -rw-r--r-- |
(* Title: ZF/epsilon.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Epsilon induction and recursion *) Epsilon = Nat + "mono" + consts eclose,rank :: "i=>i" transrec :: "[i, [i,i]=>i] =>i" defs eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" end