[isabelle-dev] Datatype alt_names

[Tobias Nipkow]

>> 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.
> 
> Do you mean the alternative names for the morphisms?  It is probably the
> standard example of explicit specification of derived names according to
> Florian's thread above.  IIRC, the "morphisms" specification is
> occasionally used in user definitions within theories, too.

It is, and one of the reasons is that the default abs/rep names can be
quite confusing (eg: which one is which?). I don't think we should get
rid of it.

Tobias