--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Types.thy Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,58 @@
+(* Title: ZF/Coind/Types.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+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]"
+
+
+(* 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]"
+
+consts
+ te_rec :: "[i,i,[i,i,i,i]=>i] => i"
+rules
+ 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))"
+
+consts
+ te_dom :: "i => i"
+ te_app :: "[i,i] => i"
+rules
+ 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))"
+
+
+end
+
+
+
+
+