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