src/ZF/Resid/Terms.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/Resid/Terms.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Resid/Terms.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Terms.thy
     1.5 +(*  Title:      Terms.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Ole Rasmussen
     1.8 +    Author:     Ole Rasmussen
     1.9      Copyright   1995  University of Cambridge
    1.10      Logic Image: ZF
    1.11  *)
    1.12 @@ -8,9 +8,9 @@
    1.13  Terms = Cube+
    1.14  
    1.15  consts
    1.16 -  lambda	:: i
    1.17 -  unmark	:: i=>i
    1.18 -  Apl		:: [i,i]=>i
    1.19 +  lambda        :: i
    1.20 +  unmark        :: i=>i
    1.21 +  Apl           :: [i,i]=>i
    1.22  
    1.23  translations
    1.24    "Apl(n,m)" == "App(0,n,m)"
    1.25 @@ -18,15 +18,15 @@
    1.26  inductive
    1.27    domains       "lambda" <= "redexes"
    1.28    intrs
    1.29 -    Lambda_Var	"               n:nat ==>     Var(n):lambda"
    1.30 -    Lambda_Fun	"            u:lambda ==>     Fun(u):lambda"
    1.31 -    Lambda_App	"[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
    1.32 -  type_intrs	"redexes.intrs@bool_typechecks"
    1.33 +    Lambda_Var  "               n:nat ==>     Var(n):lambda"
    1.34 +    Lambda_Fun  "            u:lambda ==>     Fun(u):lambda"
    1.35 +    Lambda_App  "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
    1.36 +  type_intrs    "redexes.intrs@bool_typechecks"
    1.37  
    1.38  defs
    1.39 -  unmark_def	"unmark(u) == redex_rec(u,%i.Var(i),   
    1.40 -		                          %x m.Fun(m),   
    1.41 -		                          %b x y m p.Apl(m,p))"
    1.42 +  unmark_def    "unmark(u) == redex_rec(u,%i.Var(i),   
    1.43 +                                          %x m.Fun(m),   
    1.44 +                                          %b x y m p.Apl(m,p))"
    1.45  end
    1.46  
    1.47