--- 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))"