# HG changeset patch
# User paulson
# Date 827856954 -3600
# Node ID f9a9d27e92785c70a639e7dc3546b9619b922a74
# Parent  6d7278c3f6868cc1049e2d165a708cfe287795e0
Simplified proofs, esp. for new ZF_ss

diff -r 6d7278c3f686 -r f9a9d27e9278 src/ZF/AC/Transrec2.ML
--- a/src/ZF/AC/Transrec2.ML	Tue Mar 26 16:54:09 1996 +0100
+++ b/src/ZF/AC/Transrec2.ML	Tue Mar 26 17:15:54 1996 +0100
@@ -13,13 +13,13 @@
 by (simp_tac ZF_ss 1);
 val transrec2_0 = result();
 
-goal thy "(THE j. succ(i)=succ(j)) = i";
-by (fast_tac (OrdQuant_cs addSIs [the_equality]) 1);
-val THE_succ_eq = result();
+goal thy "(THE j. i=j) = i";
+by (fast_tac (ZF_cs addSIs [the_equality]) 1);
+val THE_eq = result();
 
 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (simp_tac (ZF_ss addsimps [succ_not_0, THE_succ_eq, if_P]
+by (simp_tac (ZF_ss addsimps [succ_not_0, THE_eq, if_P]
                     setsolver K (fast_tac FOL_cs)) 1);
 val transrec2_succ = result();