src/HOL/Algebra/FiniteProduct.thy
changeset 40786 0a54cfc9add3
parent 35849 b5522b51cb1e
child 41433 1b8ff770f02c
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 28 15:20:51 2010 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4     apply (rule Suc_le_mono [THEN subst])
     1.5     apply (simp add: card_Suc_Diff1)
     1.6    apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
     1.7 -     apply (blast intro: foldSetD_imp_finite finite_Diff)
     1.8 +     apply (blast intro: foldSetD_imp_finite)
     1.9      apply best
    1.10     apply assumption
    1.11    apply (frule (1) Diff1_foldSetD)