# HG changeset patch
# User nipkow
# Date 1300352293 -3600
# Node ID c2583bbb92f519430ed366f23801f4d44bd09590
# Parent  4ad8f1dc2e0bd17a974e750655a22695f32432b3
tuned lemma

diff -r 4ad8f1dc2e0b -r c2583bbb92f5 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 16 19:50:56 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Mar 17 09:58:13 2011 +0100
@@ -1932,7 +1932,7 @@
 lemma card_Collect_less_nat[simp]: "card{i::nat. i < n} = n"
 by (induct n) (simp_all add:less_Suc_eq Collect_disj_eq)
 
-lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = n+1"
+lemma card_Collect_le_nat[simp]: "card{i::nat. i <= n} = Suc n"
 using card_Collect_less_nat[of "Suc n"] by(simp add: less_Suc_eq_le)
 
 lemma card_mono: