author | huffman |
Wed, 09 Apr 2008 05:31:04 +0200 | |
changeset 26585 | 3bf2ebb7148e |
parent 26584 | 46f3b89b2445 |
child 26586 | a2255b130fd9 |
--- 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)"