--- a/src/ZF/Resid/Terms.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Resid/Terms.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: Terms.thy
+(* Title: Terms.thy
ID: $Id$
- Author: Ole Rasmussen
+ Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
@@ -8,9 +8,9 @@
Terms = Cube+
consts
- lambda :: i
- unmark :: i=>i
- Apl :: [i,i]=>i
+ lambda :: i
+ unmark :: i=>i
+ Apl :: [i,i]=>i
translations
"Apl(n,m)" == "App(0,n,m)"
@@ -18,15 +18,15 @@
inductive
domains "lambda" <= "redexes"
intrs
- Lambda_Var " n:nat ==> Var(n):lambda"
- Lambda_Fun " u:lambda ==> Fun(u):lambda"
- Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
- type_intrs "redexes.intrs@bool_typechecks"
+ Lambda_Var " n:nat ==> Var(n):lambda"
+ Lambda_Fun " u:lambda ==> Fun(u):lambda"
+ Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
+ type_intrs "redexes.intrs@bool_typechecks"
defs
- unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
- %x m.Fun(m),
- %b x y m p.Apl(m,p))"
+ unmark_def "unmark(u) == redex_rec(u,%i.Var(i),
+ %x m.Fun(m),
+ %b x y m p.Apl(m,p))"
end