author | paulson |
Wed, 02 Apr 1997 15:30:44 +0200 | |
changeset 2874 | b1e7e2179597 |
parent 1478 | 2b8c2a7547ab |
child 3840 | e0baea4d485a |
permissions | -rw-r--r-- |
(* Title: Redex.thy ID: $Id$ Author: Ole Rasmussen Copyright 1995 University of Cambridge Logic Image: ZF *) Redex = Datatype + consts redexes :: i datatype "redexes" = Var ("n: nat") | Fun ("t: redexes") | App ("b:bool" ,"f:redexes" , "a:redexes") type_intrs "[bool_into_univ]" consts redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i defs redex_rec_def "redex_rec(p,b,c,d) == Vrec(p, %p g.redexes_case(b, %x.c(x,g`x), %n x y.d(n, x, y, g`x, g`y), p))" end