# HG changeset patch # User huffman # Date 1207711864 -7200 # Node ID 3bf2ebb7148e9b169d5ec0b4f7eb043435c4ea0d # Parent 46f3b89b2445ae3aead388a2346b867228d9536e fix spelling diff -r 46f3b89b2445 -r 3bf2ebb7148e src/HOL/Library/Countable.thy --- 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\countable \ nat" where "to_nat = (SOME f. inj f)"