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