src/ZF/Coind/Values.thy
changeset 6117 f9aad8ccd590
parent 6112 5e4871c5136b
child 11318 6536fb8c9fc6
equal deleted inserted replaced
6116:8ba2f25610f7 6117:f9aad8ccd590
    14 codatatype
    14 codatatype
    15     "Val" = v_const ("c:Const")
    15     "Val" = v_const ("c:Const")
    16           | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
    16           | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
    17   and
    17   and
    18     "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
    18     "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
    19   monos      "[map_mono]"
    19   monos       map_mono
    20   type_intrs "[A_into_univ, mapQU]"
    20   type_intrs  A_into_univ, mapQU
    21 
    21 
    22 consts
    22 consts
    23   ve_owr :: [i,i,i] => i
    23   ve_owr :: [i,i,i] => i
    24   ve_dom :: i=>i
    24   ve_dom :: i=>i
    25   ve_app :: [i,i] => i
    25   ve_app :: [i,i] => i