changeset 13149 | 773657d466cb |
parent 12814 | 2f5edb146f7e |
--- a/src/ZF/Epsilon.ML Tue May 14 12:33:42 2002 +0200 +++ b/src/ZF/Epsilon.ML Wed May 15 10:42:32 2002 +0200 @@ -314,7 +314,6 @@ Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; by (rtac (transrec2_def RS def_transrec RS trans) 1); by (simp_tac (simpset() addsimps [the_equality, if_P]) 1); -by (Blast_tac 1); qed "transrec2_succ"; Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";