src/ZF/Coind/ECR.thy
changeset 6117 f9aad8ccd590
parent 1478 2b8c2a7547ab
child 11318 6536fb8c9fc6
     1.1 --- a/src/ZF/Coind/ECR.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/Coind/ECR.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4            {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
     1.5        |] ==>   
     1.6        <v_clos(x,e,ve),t>:HasTyRel" 
     1.7 -  monos "[Pow_mono]"
     1.8 +  monos  Pow_mono
     1.9    type_intrs "Val_ValEnv.intrs"
    1.10    
    1.11  (* Pointwise extension to environments *)