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