src/ZF/Coind/Values.thy
changeset 6117 f9aad8ccd590
parent 6112 5e4871c5136b
child 11318 6536fb8c9fc6
     1.1 --- a/src/ZF/Coind/Values.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/Coind/Values.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -16,8 +16,8 @@
     1.4            | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
     1.5    and
     1.6      "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
     1.7 -  monos      "[map_mono]"
     1.8 -  type_intrs "[A_into_univ, mapQU]"
     1.9 +  monos       map_mono
    1.10 +  type_intrs  A_into_univ, mapQU
    1.11  
    1.12  consts
    1.13    ve_owr :: [i,i,i] => i