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

src/HOL/Library/Cardinality.thy

changeset 49948 | 744934b818c7 |

parent 49689 | b8a710806de9 |

child 51116 | 0dac0158b8d4 |

1.1 --- a/src/HOL/Library/Cardinality.thy Sat Oct 20 09:09:37 2012 +0200 1.2 +++ b/src/HOL/Library/Cardinality.thy Sat Oct 20 09:12:16 2012 +0200 1.3 @@ -92,7 +92,7 @@ 1.4 unfolding bs[symmetric] distinct_card[OF distb] .. 1.5 have ca: "CARD('a) = length as" 1.6 unfolding as[symmetric] distinct_card[OF dista] .. 1.7 - let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)" 1.8 + let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)" 1.9 have "UNIV = set ?xs" 1.10 proof(rule UNIV_eq_I) 1.11 fix f :: "'a \<Rightarrow> 'b" 1.12 @@ -103,8 +103,8 @@ 1.13 moreover have "distinct ?xs" unfolding distinct_map 1.14 proof(intro conjI distinct_n_lists distb inj_onI) 1.15 fix xs ys :: "'b list" 1.16 - assume xs: "xs \<in> set (Enum.n_lists (length as) bs)" 1.17 - and ys: "ys \<in> set (Enum.n_lists (length as) bs)" 1.18 + assume xs: "xs \<in> set (List.n_lists (length as) bs)" 1.19 + and ys: "ys \<in> set (List.n_lists (length as) bs)" 1.20 and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)" 1.21 from xs ys have [simp]: "length xs = length as" "length ys = length as" 1.22 by(simp_all add: length_n_lists_elem) 1.23 @@ -472,3 +472,4 @@ 1.24 hide_const (open) card' finite' subset' eq_set 1.25 1.26 end 1.27 +