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