Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/FiniteProduct.thy
changeset 40786 0a54cfc9add3
parent 35849 b5522b51cb1e
child 41433 1b8ff770f02c 
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -130,7 +130,7 @@
    apply (rule Suc_le_mono [THEN subst])
    apply (simp add: card_Suc_Diff1)
   apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
-     apply (blast intro: foldSetD_imp_finite finite_Diff)
+     apply (blast intro: foldSetD_imp_finite)
     apply best
    apply assumption
   apply (frule (1) Diff1_foldSetD)
isabelle