[isabelle-dev] Datatype alt_names

[Brian Huffman]

On Wed, Nov 3, 2010 at 5:56 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> 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

I brought up this issue on the mailing list last year:

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-May/000578.html

I have since removed a similar feature from the HOLCF domain package.

It seems to me that such a feature could only be justified if it was
needed for backward compatibility. But since this feature was broken
in more than one released version of Isabelle, and nobody has ever
complained about it, backward compatibility is not an issue for
anyone.

- Brian

P. S.

The 'typedef' command supports a similar option for alternative names;
I am sure that it was originally created for use with non-alphanumeric
type names. One could also ask whether the existence of this feature
for typedef is still justified, when all types have regular names now.