I am not sure whether this is relevant, but I have recently introduced a similar feature in Nominal2. There the problem is that one often defines several mutual-recursive nominal datatypes, like
nominal_datatype foo1 = .. and foo2 = .. .... and foon = .. with n being a non-trivial number like 5 or even more. The problem with this is that the generated theorems have names like foo1_foo2_....._foon.induct This naming scheme is not very user-friendly. So I decided to allow nominal_datatype (bar) foo1 = .. and foo2 = .. .... and foon = .. to produce bar.induct etc instead. I do not know of anything else that would allow the user to have control over the generated theorem names. Is this something which goes against all Isabelle conventions? Could this be helpful for "normal" datatypes? Best wishes, Christian Florian Haftmann writes: > Traditionally the datatype command would accept optional "alternative > names" used in names of type-related facts etc., e.g. > > datatype (foo) "/*/" = Bar > > With all HOL types being regulary named, the question arises whether we > still have to keep that feature or shall just discontinue it? > > Florian > > -- > > Home: > http://www.in.tum.de/~haftmann > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev@mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev