src/HOL/Finite_Set.thy
changeset 14443 75910c7557c5
parent 14430 5cb24165a2e1
child 14449 d5c3d21df790
--- a/src/HOL/Finite_Set.thy	Mon Mar 08 11:11:58 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 08 11:12:06 2004 +0100
@@ -1423,4 +1423,5 @@
     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   by (simp add: n_sub_lemma)
 
+
 end