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

src/HOL/Library/Countable.thy

changeset 28823 | dcbef866c9e2 |

parent 27487 | c8a6ce181805 |

child 29511 | 7071b017cb35 |

--- a/src/HOL/Library/Countable.thy Mon Nov 17 17:00:27 2008 +0100 +++ b/src/HOL/Library/Countable.thy Mon Nov 17 17:00:55 2008 +0100 @@ -49,7 +49,7 @@ by (rule countable_classI [of "id"]) simp subclass (in finite) countable -proof unfold_locales +proof have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) with finite_conv_nat_seg_image [of UNIV] obtain n and f :: "nat \<Rightarrow> 'a"