changeset 37388 | 793618618f78 |
parent 35700 | 951974ce903e |
child 37652 | 6aa09d2a6cf9 |
--- a/src/HOL/Library/Countable.thy Tue Jun 08 16:37:19 2010 +0200 +++ b/src/HOL/Library/Countable.thy Tue Jun 08 16:37:22 2010 +0200 @@ -70,7 +70,7 @@ text {* Sums *} -instance "+":: (countable, countable) countable +instance "+" :: (countable, countable) countable by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) | Inr b \<Rightarrow> to_nat (True, to_nat b))"]) (simp split: sum.split_asm)