| changeset 13615 | 449a70d88b38 |
| parent 13524 | 604d0f3622d6 |
| child 13784 | b9f6154427a4 |
--- a/src/ZF/Cardinal.thy Tue Oct 01 11:17:25 2002 +0200 +++ b/src/ZF/Cardinal.thy Tue Oct 01 13:26:10 2002 +0200 @@ -917,8 +917,7 @@ apply (erule Finite_induct, auto) apply (case_tac "x:A") apply (subgoal_tac [2] "A-cons (x, B) = A - B") -apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}") -apply (rotate_tac -1, simp) +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp) apply (drule Diff_sing_Finite, auto) done