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/Number_Theory/Binomial.thy
changeset 35731 1bdaa24fb56d
parent 35644 d20cf282342e
child 36350 bc7982c54e37 
--- a/src/HOL/Number_Theory/Binomial.thy	Thu Mar 11 15:52:34 2010 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy	Thu Mar 11 15:52:35 2010 +0100
@@ -364,7 +364,7 @@
         finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
           card F choose (k + 1) + (card F choose k)".
         with iassms choose_plus_one_nat show ?thesis
-          by auto
+          by (auto simp del: card.insert)
       qed
     qed
   qed
isabelle