src/HOL/Library/Countable.thy
changeset 29797 08ef36ed2f8a
parent 29511 7071b017cb35
child 29880 3dee8ff45d3d
     1.1 --- a/src/HOL/Library/Countable.thy	Tue Feb 03 19:48:06 2009 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Tue Feb 03 21:26:21 2009 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection {* The class of countable types *}
     1.6  
     1.7 -class countable = itself +
     1.8 +class countable =
     1.9    assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
    1.10  
    1.11  lemma countable_classI: