# HG changeset patch
# User lcp
# Date 794579673 -3600
# Node ID 2e0203309287293f346b8294a0a1389968ed013b
# Parent  5836531d7b9156cf68ca9e57471df89841cf930f
Replaced rules by defs.  Also got rid of tyconstU by
including TyConst in the datatype's universe

diff -r 5836531d7b91 -r 2e0203309287 src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Tue Mar 07 13:32:22 1995 +0100
+++ b/src/ZF/Coind/Types.thy	Tue Mar 07 13:34:33 1995 +0100
@@ -6,38 +6,25 @@
 
 Types = Language +
 
-(* Abstract type of type constants *)
-  
 consts
-  TyConst :: "i"
-rules
-  tyconstU "tc:TyConst ==> tc:univ(0)"
-
-
-(* Datatype of types *)
-  
-consts
-  Ty :: "i"
-datatype
-  "Ty" =
-    t_const("tc:TyConst") |
-    t_fun("t1:Ty","t2:Ty")
-  type_intrs "[tyconstU]"
+  Ty :: "i"			(* Datatype of types *)
+  TyConst :: "i"		(* Abstract type of type constants *)
+datatype <= "univ(TyConst)"
+  "Ty" = t_const("tc:TyConst")
+       | t_fun("t1:Ty","t2:Ty")
   
 
 (* Definition of type environments and associated operators *)
 
 consts
   TyEnv :: "i"
-datatype
-  "TyEnv" =
-     te_emp |
-     te_owr("te:TyEnv","x:ExVar","t:Ty") 
-  type_intrs "[exvarU,Ty.dom_subset RS subsetD]"
+datatype <= "univ(Ty Un ExVar)"
+  "TyEnv" = te_emp
+          | te_owr("te:TyEnv","x:ExVar","t:Ty") 
 
 consts
   te_rec :: "[i,i,[i,i,i,i]=>i] => i"
-rules
+defs
   te_rec_def
     "te_rec(te,c,h) ==   \
 \    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
@@ -45,7 +32,7 @@
 consts
   te_dom :: "i => i"
   te_app :: "[i,i] => i"
-rules
+defs
   te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
   te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"