[isabelle-dev] Datatype alt_names
nipkow at in.tum.de
Wed Nov 3 16:26:15 CET 2010
>> 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.
More information about the isabelle-dev