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