src/HOL/Library/Countable.thy
changeset 58155 14dda84afbb3
parent 58112 8081087096ad
child 58158 d2cb7cbb3aaa
equal deleted inserted replaced
58154:47c3c7019b97 58155:14dda84afbb3
   306 *} "prove countable class instances for datatypes"
   306 *} "prove countable class instances for datatypes"
   307 
   307 
   308 hide_const (open) finite_item nth_item
   308 hide_const (open) finite_item nth_item
   309 
   309 
   310 
   310 
       
   311 (* FIXME
   311 subsection {* Countable datatypes *}
   312 subsection {* Countable datatypes *}
   312 
   313 
   313 instance typerep :: countable
   314 instance typerep :: countable
   314   by countable_datatype
   315   by countable_datatype
       
   316 *)
   315 
   317 
   316 end
   318 end