--- a/src/ZF/Coind/ECR.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Coind/ECR.thy Thu Jun 22 17:13:05 1995 +0200
@@ -16,12 +16,12 @@
htr_constI
"[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
htr_closI
- "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
-\ <te,e_fn(x,e),t>:ElabRel; \
-\ ve_dom(ve) = te_dom(te); \
-\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel) \
-\ |] ==> \
-\ <v_clos(x,e,ve),t>:HasTyRel"
+ "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv;
+ <te,e_fn(x,e),t>:ElabRel;
+ ve_dom(ve) = te_dom(te);
+ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)
+ |] ==>
+ <v_clos(x,e,ve),t>:HasTyRel"
monos "[Pow_mono]"
type_intrs "Val_ValEnv.intrs"
@@ -31,8 +31,8 @@
hastyenv :: "[i,i] => o"
defs
hastyenv_def
- " hastyenv(ve,te) == \
-\ ve_dom(ve) = te_dom(te) & \
-\ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+ " hastyenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
end