summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Cardinality.thy

changeset 49948 | 744934b818c7 |

parent 49689 | b8a710806de9 |

child 51116 | 0dac0158b8d4 |

--- a/src/HOL/Library/Cardinality.thy Sat Oct 20 09:09:37 2012 +0200 +++ b/src/HOL/Library/Cardinality.thy Sat Oct 20 09:12:16 2012 +0200 @@ -92,7 +92,7 @@ unfolding bs[symmetric] distinct_card[OF distb] .. have ca: "CARD('a) = length as" unfolding as[symmetric] distinct_card[OF dista] .. - let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)" + let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)" have "UNIV = set ?xs" proof(rule UNIV_eq_I) fix f :: "'a \<Rightarrow> 'b" @@ -103,8 +103,8 @@ moreover have "distinct ?xs" unfolding distinct_map proof(intro conjI distinct_n_lists distb inj_onI) fix xs ys :: "'b list" - assume xs: "xs \<in> set (Enum.n_lists (length as) bs)" - and ys: "ys \<in> set (Enum.n_lists (length as) bs)" + assume xs: "xs \<in> set (List.n_lists (length as) bs)" + and ys: "ys \<in> set (List.n_lists (length as) bs)" and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)" from xs ys have [simp]: "length xs = length as" "length ys = length as" by(simp_all add: length_n_lists_elem) @@ -472,3 +472,4 @@ hide_const (open) card' finite' subset' eq_set end +