1.1 --- a/src/HOL/Library/Countable.thy	Wed Jul 27 19:34:30 2011 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Wed Jul 27 19:35:00 2011 +0200
     1.3 @@ -35,6 +35,9 @@
     1.4  lemma inj_to_nat [simp]: "inj to_nat"
     1.5    by (rule exE_some [OF ex_inj]) (simp add: to_nat_def)
     1.6  
     1.7 +lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S"
     1.8 +  using inj_to_nat by (auto simp: inj_on_def)
     1.9 +
    1.10  lemma surj_from_nat [simp]: "surj from_nat"
    1.11    unfolding from_nat_def by (simp add: inj_imp_surj_inv)
    1.12