src/ZF/Resid/Residuals.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/Resid/Residuals.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Resid/Residuals.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Residuals.thy
     1.5 +(*  Title:      Residuals.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 @@ -9,9 +9,9 @@
    1.13  Residuals = Substitution+
    1.14  
    1.15  consts
    1.16 -  Sres		:: i
    1.17 -  residuals	:: [i,i,i]=>i
    1.18 -  "|>"		:: [i,i]=>i     (infixl 70)
    1.19 +  Sres          :: i
    1.20 +  residuals     :: [i,i,i]=>i
    1.21 +  "|>"          :: [i,i]=>i     (infixl 70)
    1.22    
    1.23  translations
    1.24    "residuals(u,v,w)"  == "<u,v,w>:Sres"
    1.25 @@ -19,16 +19,16 @@
    1.26  inductive
    1.27    domains       "Sres" <= "redexes*redexes*redexes"
    1.28    intrs
    1.29 -    Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
    1.30 -    Res_Fun	"[|residuals(u,v,w)|]==>   
    1.31 -		     residuals(Fun(u),Fun(v),Fun(w))"
    1.32 -    Res_App	"[|residuals(u1,v1,w1);   
    1.33 -		   residuals(u2,v2,w2); b:bool|]==>   
    1.34 -		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
    1.35 -    Res_redex	"[|residuals(u1,v1,w1);   
    1.36 -		   residuals(u2,v2,w2); b:bool|]==>   
    1.37 -		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
    1.38 -  type_intrs	"[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
    1.39 +    Res_Var     "n:nat ==> residuals(Var(n),Var(n),Var(n))"
    1.40 +    Res_Fun     "[|residuals(u,v,w)|]==>   
    1.41 +                     residuals(Fun(u),Fun(v),Fun(w))"
    1.42 +    Res_App     "[|residuals(u1,v1,w1);   
    1.43 +                   residuals(u2,v2,w2); b:bool|]==>   
    1.44 +                 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
    1.45 +    Res_redex   "[|residuals(u1,v1,w1);   
    1.46 +                   residuals(u2,v2,w2); b:bool|]==>   
    1.47 +                 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
    1.48 +  type_intrs    "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
    1.49  
    1.50  rules
    1.51    res_func_def  "u |> v == THE w.residuals(u,v,w)"