src/HOL/List.thy
changeset 52141 eff000cab70f
parent 52131 366fa32ee2a3
child 52148 893b15200ec1
     1.1 --- a/src/HOL/List.thy	Sat May 25 15:44:08 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Sat May 25 15:44:29 2013 +0200
     1.3 @@ -4312,7 +4312,7 @@
     1.4    moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
     1.5      by (simp add: card_Diff_subset distinct_card)
     1.6    moreover have "{xs. ?k_list (Suc k) xs} =
     1.7 -      (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
     1.8 +      (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
     1.9      by (auto simp: length_Suc_conv)
    1.10    moreover
    1.11    have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp