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

src/HOL/Library/Cardinality.thy

changeset 67091 | 1393c2340eec |

parent 62597 | b3f2b8c906a6 |

child 67399 | eab6ce8368fa |

1.1 --- a/src/HOL/Library/Cardinality.thy Sun Nov 26 13:19:52 2017 +0100 1.2 +++ b/src/HOL/Library/Cardinality.thy Sun Nov 26 21:08:32 2017 +0100 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)) (List.n_lists (length as) bs)" 1.8 + let ?xs = "map (\<lambda>ys. the \<circ> 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"