--- a/src/ZF/ex/Limit.thy Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Limit.thy Sat Dec 09 13:36:11 1995 +0100
@@ -21,43 +21,43 @@
consts
- "rel" :: "[i,i,i]=>o" (* rel(D,x,y) *)
- "set" :: "i=>i" (* set(D) *)
- "po" :: "i=>o" (* po(D) *)
- "chain" :: "[i,i]=>o" (* chain(D,X) *)
- "isub" :: "[i,i,i]=>o" (* isub(D,X,x) *)
- "islub" :: "[i,i,i]=>o" (* islub(D,X,x) *)
- "lub" :: "[i,i]=>i" (* lub(D,X) *)
- "cpo" :: "i=>o" (* cpo(D) *)
- "pcpo" :: "i=>o" (* pcpo(D) *)
- "bot" :: "i=>i" (* bot(D) *)
- "mono" :: "[i,i]=>i" (* mono(D,E) *)
- "cont" :: "[i,i]=>i" (* cont(D,E) *)
- "cf" :: "[i,i]=>i" (* cf(D,E) *)
+ "rel" :: [i,i,i]=>o (* rel(D,x,y) *)
+ "set" :: i=>i (* set(D) *)
+ "po" :: i=>o (* po(D) *)
+ "chain" :: [i,i]=>o (* chain(D,X) *)
+ "isub" :: [i,i,i]=>o (* isub(D,X,x) *)
+ "islub" :: [i,i,i]=>o (* islub(D,X,x) *)
+ "lub" :: [i,i]=>i (* lub(D,X) *)
+ "cpo" :: i=>o (* cpo(D) *)
+ "pcpo" :: i=>o (* pcpo(D) *)
+ "bot" :: i=>i (* bot(D) *)
+ "mono" :: [i,i]=>i (* mono(D,E) *)
+ "cont" :: [i,i]=>i (* cont(D,E) *)
+ "cf" :: [i,i]=>i (* cf(D,E) *)
- "suffix" :: "[i,i]=>i" (* suffix(X,n) *)
- "subchain" :: "[i,i]=>o" (* subchain(X,Y) *)
- "dominate" :: "[i,i,i]=>o" (* dominate(D,X,Y) *)
- "matrix" :: "[i,i]=>o" (* matrix(D,M) *)
+ "suffix" :: [i,i]=>i (* suffix(X,n) *)
+ "subchain" :: [i,i]=>o (* subchain(X,Y) *)
+ "dominate" :: [i,i,i]=>o (* dominate(D,X,Y) *)
+ "matrix" :: [i,i]=>o (* matrix(D,M) *)
- "projpair" :: "[i,i,i,i]=>o" (* projpair(D,E,e,p) *)
- "emb" :: "[i,i,i]=>o" (* emb(D,E,e) *)
- "Rp" :: "[i,i,i]=>i" (* Rp(D,E,e) *)
- "iprod" :: "i=>i" (* iprod(DD) *)
- "mkcpo" :: "[i,i=>o]=>i" (* mkcpo(D,P) *)
- "subcpo" :: "[i,i]=>o" (* subcpo(D,E) *)
- "subpcpo" :: "[i,i]=>o" (* subpcpo(D,E) *)
+ "projpair" :: [i,i,i,i]=>o (* projpair(D,E,e,p) *)
+ "emb" :: [i,i,i]=>o (* emb(D,E,e) *)
+ "Rp" :: [i,i,i]=>i (* Rp(D,E,e) *)
+ "iprod" :: i=>i (* iprod(DD) *)
+ "mkcpo" :: [i,i=>o]=>i (* mkcpo(D,P) *)
+ "subcpo" :: [i,i]=>o (* subcpo(D,E) *)
+ "subpcpo" :: [i,i]=>o (* subpcpo(D,E) *)
- "emb_chain" :: "[i,i]=>o" (* emb_chain(DD,ee) *)
- "Dinf" :: "[i,i]=>i" (* Dinf(DD,ee) *)
+ "emb_chain" :: [i,i]=>o (* emb_chain(DD,ee) *)
+ "Dinf" :: [i,i]=>i (* Dinf(DD,ee) *)
- "e_less" :: "[i,i,i,i]=>i" (* e_less(DD,ee,m,n) *)
- "e_gr" :: "[i,i,i,i]=>i" (* e_gr(DD,ee,m,n) *)
- "eps" :: "[i,i,i,i]=>i" (* eps(DD,ee,m,n) *)
- "rho_emb" :: "[i,i,i]=>i" (* rho_emb(DD,ee,n) *)
- "rho_proj" :: "[i,i,i]=>i" (* rho_proj(DD,ee,n) *)
- "commute" :: "[i,i,i,i=>i]=>o" (* commute(DD,ee,E,r) *)
- "mediating" :: "[i,i,i=>i,i=>i,i]=>o" (* mediating(E,G,r,f,t) *)
+ "e_less" :: [i,i,i,i]=>i (* e_less(DD,ee,m,n) *)
+ "e_gr" :: [i,i,i,i]=>i (* e_gr(DD,ee,m,n) *)
+ "eps" :: [i,i,i,i]=>i (* eps(DD,ee,m,n) *)
+ "rho_emb" :: [i,i,i]=>i (* rho_emb(DD,ee,n) *)
+ "rho_proj" :: [i,i,i]=>i (* rho_proj(DD,ee,n) *)
+ "commute" :: [i,i,i,i=>i]=>o (* commute(DD,ee,E,r) *)
+ "mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *)
rules