>> 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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
