src/ZF/Coind/ECR.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
     1.1 --- a/src/ZF/Coind/ECR.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Coind/ECR.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/Coind/ECR.thy
     1.5 +(*  Title:      ZF/Coind/ECR.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     1.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
     1.9      Copyright   1995  University of Cambridge
    1.10  *)
    1.11  
    1.12 @@ -17,9 +17,9 @@
    1.13        "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
    1.14      htr_closI
    1.15        "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
    1.16 -	  <te,e_fn(x,e),t>:ElabRel;  
    1.17 -	  ve_dom(ve) = te_dom(te);   
    1.18 -	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
    1.19 +          <te,e_fn(x,e),t>:ElabRel;  
    1.20 +          ve_dom(ve) = te_dom(te);   
    1.21 +          {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
    1.22        |] ==>   
    1.23        <v_clos(x,e,ve),t>:HasTyRel" 
    1.24    monos "[Pow_mono]"
    1.25 @@ -31,8 +31,8 @@
    1.26    hastyenv :: [i,i] => o
    1.27  defs
    1.28    hastyenv_def 
    1.29 -    " hastyenv(ve,te) == 			
    1.30 -     ve_dom(ve) = te_dom(te) & 		
    1.31 +    " hastyenv(ve,te) ==                        
    1.32 +     ve_dom(ve) = te_dom(te) &          
    1.33       (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
    1.34  
    1.35  end