src/HOL/Library/Permutations.thy
changeset 61424 c3658c18b7bc
parent 60601 6e83d94760c4
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/Permutations.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4        by (auto intro: card_ge_0_finite)
     1.5      then have pF'f: "finite ?pF'"
     1.6        using H0 \<open>finite F\<close>
     1.7 -      apply (simp only: Collect_split Collect_mem_eq)
     1.8 +      apply (simp only: Collect_case_prod Collect_mem_eq)
     1.9        apply (rule finite_cartesian_product)
    1.10        apply simp_all
    1.11        done
    1.12 @@ -246,7 +246,7 @@
    1.13      from pFs H0 have xFc: "card ?xF = fact n"
    1.14        unfolding xfgpF' card_image[OF ginj]
    1.15        using \<open>finite F\<close> \<open>finite ?pF\<close>
    1.16 -      apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
    1.17 +      apply (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product)
    1.18        apply simp
    1.19        done
    1.20      from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"