# HG changeset patch
# User nipkow
# Date 1288769372 -3600
# Node ID 994e784ca17a958cc86af89cbebcebe976f57668
# Parent  a0698ec82e6ee6d58ec66a53d0be799357afdb87
removed assumption

diff -r a0698ec82e6e -r 994e784ca17a src/HOL/Finite_Set.thy
--- 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: