src/ZF/Resid/Redex.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2874 b1e7e2179597
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      Redex.thy
     2     ID:         $Id$
     3     Author:     Ole Rasmussen
     4     Copyright   1995  University of Cambridge
     5     Logic Image: ZF
     6 *)
     7 
     8 Redex = Univ +
     9 consts
    10   redexes     :: i
    11 
    12 datatype
    13   "redexes" = Var ("n: nat")            
    14             | Fun ("t: redexes")
    15             | App ("b:bool" ,"f:redexes" , "a:redexes")
    16   type_intrs "[bool_into_univ]"
    17   
    18 
    19 consts
    20   redex_rec     :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
    21  
    22 defs
    23   redex_rec_def
    24    "redex_rec(p,b,c,d) == 
    25    Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
    26                              %n x y.d(n, x, y, g`x, g`y), p))"
    27 end
    28