Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed assumption
authornipkow
Wed, 03 Nov 2010 08:29:32 +0100
changeset 40311 994e784ca17a
parent 40310 a0698ec82e6e
child 40312 dff9f73a3763
child 40320 abc52faa7761
removed assumption
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite_Set.thy	Tue Nov 02 21:59:21 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Nov 03 08:29:32 2010 +0100
@@ -2182,7 +2182,7 @@
 
 subsubsection {* Pigeonhole Principles *}
 
-lemma pigeonhole: "finite(A) \<Longrightarrow> card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
+lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
 by (auto dest: card_image less_irrefl_nat)
 
 lemma pigeonhole_infinite:
isabelle