[isabelle-dev] Countable instantiation addition

[Alexander Krauss]

> datatype foo = ....
> deriving countable, finite,

Tobias also mentioned "set_of", "map_of", etc. But since these aren't 
class instantiations (we have no constructor classes such as "functor"), 
we end up with the good old generic datatype interpretation (roughly: 
datatype -> theory -> theory).

So it seems like we simply want named datatype interpretations that are 
explicitly invoked via "deriving" (stretching the original Haskell 
notion quite a bit...)

Alex