src/ZF/Epsilon.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
equal deleted inserted replaced
13327:be7105a066d3 13328:703de709a64b
     1 (*  Title:      ZF/epsilon.thy
     1 (*  Title:      ZF/epsilon.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Epsilon induction and recursion
       
     7 *)
     6 *)
       
     7 
       
     8 header{*Epsilon Induction and Recursion*}
     8 
     9 
     9 theory Epsilon = Nat + mono:
    10 theory Epsilon = Nat + mono:
    10 
    11 
    11 constdefs
    12 constdefs
    12   eclose    :: "i=>i"
    13   eclose    :: "i=>i"