--- a/src/ZF/Coind/Values.thy Tue Mar 07 13:29:36 1995 +0100
+++ b/src/ZF/Coind/Values.thy Tue Mar 07 13:32:22 1995 +0100
@@ -9,22 +9,21 @@
(* Values, values environments and associated operators *)
consts
- Val :: "i" ValEnv :: "i" Val_ValEnv :: "i"
-codatatype
- "Val" =
- v_const("c:Const") |
- v_clos("x:ExVar","e:Exp","ve:ValEnv") and
- "ValEnv" =
- ve_mk("m:PMap(ExVar,Val)")
- monos "[map_mono]"
- type_intrs "[constQU,exvarQU,exvarU,expQU,mapQU]"
+ Val, ValEnv, Val_ValEnv :: "i"
+codatatype <= "quniv(Const Un ExVar Un Exp)"
+ "Val" = v_const("c:Const")
+ | 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]"
consts
ve_emp :: "i"
ve_owr :: "[i,i,i] => i"
ve_dom :: "i=>i"
ve_app :: "[i,i] => i"
-rules
+defs
ve_emp_def "ve_emp == ve_mk(map_emp)"
ve_owr_def
"ve_owr(ve,x,v) == \