[isabelle-dev] [isabelle] Countable instantiation addition

[Alexander Krauss]

Hi Matthieu,

> I have written a little ML library allowing to automatically prove, in most
> cases, instantiations of types (typedefs, records and datatypes) as countable
> (see ~~/src/HOL/Library/Countable).

It seems that for datatypes we now have such functionality, implemented 
four weeks ago by Brian Huffman:

http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f

It comes in the form of a method, so it has to be invoked explicitly, 
but like this it doesn't produce any penalty when it is not used. If you 
want to contribute an extension to records/typedefs, you are welcome, 
but you probably want to study Brian's implementation first. I assume 
that he is also the most appropriate person to review patches for this 
functionality.

Alex