# HG changeset patch
# User lcp
# Date 794579542 -3600
# Node ID 5836531d7b9156cf68ca9e57471df89841cf930f
# Parent  b7ab0425332696ba7c364d44e732a8bfaf71c341
Replaced rules by defs

diff -r b7ab04253326 -r 5836531d7b91 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Mar 07 13:29:36 1995 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Mar 07 13:32:22 1995 +0100
@@ -9,7 +9,7 @@
 consts
   TMap :: "[i,i] => i"
   PMap :: "[i,i] => i"
-rules
+defs
   TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
   PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
 
@@ -19,7 +19,7 @@
   map_emp :: "i"
   map_owr :: "[i,i,i]=>i"
   map_app :: "[i,i]=>i"
-rules
+defs
   map_emp_def "map_emp == 0"
   map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
   map_app_def "map_app(m,a) == m``{a}"
diff -r b7ab04253326 -r 5836531d7b91 src/ZF/Coind/Values.thy
--- 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) ==   \