On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote: > ....I.e. everything that is defined by the new package and > falls into the fragment of the old package can be registered as an old > datatype benefiting from all the infrastructure built around it (e.g. > size function, Quickcheck, and other "datatype interpretations").
On the topic of size functions: I found it always odd that the existing datatype package (however I think this particular functionality is now provided by the function package) defines under <datatype_name>.simps "two" definitions of the corresponding size function. Consider for example datatype test = A1 | A2 | A3 "test" thm test.size > test_size A1 = 0 > test_size A2 = 0 > test_size (A3 ?test) = test_size ?test + Suc 0 > size A1 = 0 > size A2 = 0 > size (A3 ?test) = size ?test + Suc 0 Surely, it would be more uniform to have just the equations for size, no? Is there any usage for the test_size definitions? If not, then maybe in the course of updating the datatype package, this oddity can be eliminated (Nominal needed to work around it). But I am happy to admit that I might miss something important. Best wishes, Christian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev