author | wenzelm |
Fri, 10 Oct 1997 18:23:31 +0200 | |
changeset 3840 | e0baea4d485a |
parent 2874 | b1e7e2179597 |
child 6046 | 2c8a8be36c94 |
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