| changeset 46471 | 2289a3869c88 |
| parent 45602 | 2a858377c3d2 |
| child 46751 | 6b94c39b7366 |
--- a/src/ZF/Cardinal.thy Tue Feb 14 20:57:05 2012 +0100 +++ b/src/ZF/Cardinal.thy Tue Feb 14 21:19:39 2012 +0100 @@ -869,7 +869,7 @@ apply (simp add: eqpoll_0_iff, clarify) apply (subgoal_tac "EX u. u:A") apply (erule exE) -apply (rule Diff_sing_eqpoll [THEN revcut_rl]) +apply (rule Diff_sing_eqpoll [elim_format]) prefer 2 apply assumption apply assumption apply (rule_tac b = A in cons_Diff [THEN subst], assumption)