# HG changeset patch
# User lcp
# Date 783863022 -3600
# Node ID 0ca24b09f4a6243d5d2c4437a603243373139144
# Parent  b9fc536792bbb2789b5d688edb81ab5b86c04377
ZF/InfDatatype/fun_Vcsucc: removed use of PiE

diff -r b9fc536792bb -r 0ca24b09f4a6 src/ZF/InfDatatype.ML
--- a/src/ZF/InfDatatype.ML	Thu Nov 03 12:39:39 1994 +0100
+++ b/src/ZF/InfDatatype.ML	Thu Nov 03 12:43:42 1994 +0100
@@ -127,7 +127,7 @@
 \         W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
 by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
 by (resolve_tac [Vfrom RS ssubst] 1);
-by (eresolve_tac [PiE] 1);
+by (dresolve_tac [fun_is_rel] 1);
 (*This level includes the function, and is below csucc(K)*)
 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
 by (eresolve_tac [subset_trans RS PowI] 2);