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

src/HOL/Library/Countable.thy

changeset 31992 | f8aed98faae7 |

parent 30663 | 0b6aff7451b2 |

child 33640 | 0d82107dc07a |

--- a/src/HOL/Library/Countable.thy Fri Jul 10 09:24:50 2009 +0200 +++ b/src/HOL/Library/Countable.thy Sun Jul 12 10:14:51 2009 +0200 @@ -58,7 +58,7 @@ subclass (in finite) countable proof have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) - with finite_conv_nat_seg_image [of UNIV] + with finite_conv_nat_seg_image [of "UNIV::'a set"] obtain n and f :: "nat \<Rightarrow> 'a" where "UNIV = f ` {i. i < n}" by auto then have "surj f" unfolding surj_def by auto