src/HOL/Library/Countable.thy
changeset 58155 14dda84afbb3
parent 58112 8081087096ad
child 58158 d2cb7cbb3aaa
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:26 2014 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Wed Sep 03 00:06:27 2014 +0200
     1.3 @@ -308,9 +308,11 @@
     1.4  hide_const (open) finite_item nth_item
     1.5  
     1.6  
     1.7 +(* FIXME
     1.8  subsection {* Countable datatypes *}
     1.9  
    1.10  instance typerep :: countable
    1.11    by countable_datatype
    1.12 +*)
    1.13  
    1.14  end