changeset 44890 | 22f665a2e91c |
parent 44279 | 7496258e44e4 |
child 45969 | 562e99c3d316 |
--- a/src/HOL/Equiv_Relations.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Equiv_Relations.thy Mon Sep 12 07:55:43 2011 +0200 @@ -349,7 +349,7 @@ apply(subst card_UN_disjoint) apply assumption apply simp - apply(fastsimp simp add:inj_on_def) + apply(fastforce simp add:inj_on_def) apply simp done