src/ZF/Resid/Residuals.thy

 
 inductive
   domains       "Sres" <= "redexes*redexes*redexes"
   intrs
     Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
-    Res_Fun	"[|residuals(u,v,w)|]==>   \
-\		     residuals(Fun(u),Fun(v),Fun(w))"
-    Res_App	"[|residuals(u1,v1,w1);   \
-\		   residuals(u2,v2,w2); b:bool|]==>   \
-\		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
-    Res_redex	"[|residuals(u1,v1,w1);   \
-\		   residuals(u2,v2,w2); b:bool|]==>   \
-\		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
+    Res_Fun	"[|residuals(u,v,w)|]==>   
+		     residuals(Fun(u),Fun(v),Fun(w))"
+    Res_App	"[|residuals(u1,v1,w1);   
+		   residuals(u2,v2,w2); b:bool|]==>   
+		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
+    Res_redex	"[|residuals(u1,v1,w1);   
+		   residuals(u2,v2,w2); b:bool|]==>   
+		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   type_intrs	"[subst_type]@[e-mail]@bool_typechecks"
 
 rules
   res_func_def  "u |> v == THE w.residuals(u,v,w)"
 end