summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"