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 +