[isabelle-dev] [isabelle] Countable instantiation addition

Alexander Krauss krauss at in.tum.de
Thu Jul 21 20:15:19 CEST 2011

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:


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 


More information about the isabelle-dev mailing list