| changeset 3724 | f33e301a89f5 |
| parent 3708 | 56facaebf3e3 |
| child 3842 | b55686a7b22c |
--- a/src/HOL/Finite.ML Mon Sep 29 11:36:44 1997 +0200 +++ b/src/HOL/Finite.ML Mon Sep 29 11:37:02 1997 +0200 @@ -378,7 +378,7 @@ goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A"; by (etac finite_induct 1); by (ALLGOALS Asm_simp_tac); -by (Step_tac 1); +by Safe_tac; by (rewtac inj_onto_def); by (Blast_tac 1); by (stac card_insert_disjoint 1);