Re: [isabelle-dev] Countable instantiation addition

2011-07-22 Thread 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

Re: [isabelle-dev] Countable instantiation addition

2011-07-22 Thread Lukas Bulwahn
On 07/22/2011 09:36 AM, Alexander Krauss wrote: 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

Re: [isabelle-dev] Countable instantiation addition

2011-07-22 Thread Lukas Bulwahn
On 07/22/2011 10:44 AM, Lukas Bulwahn wrote: On 07/22/2011 09:36 AM, Alexander Krauss wrote: 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