author | clasohm |
Thu, 16 Sep 1993 12:20:38 +0200 | |
changeset 0 | a5a9c433f639 |
child 124 | 858ab9a9b047 |
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 + consts eclose,rank :: "i=>i" transrec :: "[i, [i,i]=>i] =>i" rules 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