changeset 44890 | 22f665a2e91c |
parent 44872 | a98ef45122f3 |
child 53374 | a14d2a854c02 |
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy Mon Sep 12 07:55:43 2011 +0200 @@ -259,7 +259,7 @@ apply blast apply (erule finite_UN_I) apply blast - apply (fastsimp) + apply (fastforce) apply (auto intro!: funcsetI finprod_closed) done