changeset 26585 | 3bf2ebb7148e |
parent 26580 | c3e597a476fd |
child 27368 | 9f90ac19e32b |
--- a/src/HOL/Library/Countable.thy Wed Apr 09 05:30:14 2008 +0200 +++ b/src/HOL/Library/Countable.thy Wed Apr 09 05:31:04 2008 +0200 @@ -24,7 +24,7 @@ qed -subsection {* Converion functions *} +subsection {* Conversion functions *} definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where "to_nat = (SOME f. inj f)"