1.1 --- a/src/HOL/Library/Countable.thy	Sun Mar 09 07:57:30 2008 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Mon Mar 10 18:44:20 2008 +0100
     1.3 @@ -180,4 +180,18 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +
     1.8 +text {* Functions *}
     1.9 +
    1.10 +instance "fun" :: (finite, countable) countable
    1.11 +proof
    1.12 +  obtain xs :: "'a list" where xs: "set xs = UNIV"
    1.13 +    using finite_list [OF finite_UNIV] ..
    1.14 +  show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
    1.15 +  proof
    1.16 +    show "inj (\<lambda>f. to_nat (map f xs))"
    1.17 +      by (rule injI, simp add: xs expand_fun_eq)
    1.18 +  qed
    1.19 +qed
    1.20 +
    1.21  end