Re: [mizar] Now I know why I cannot quote a theorem but the trouble remains

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

On Sun, 30 Nov 2003, Freek Wiedijk wrote:

> >This brings back the issue of Universal Resource Naming (URN).  I am
> >in favour of using Grzegorz's names from MML Query and I would put up
> >with writing something like this:
> >
> >  URN(POLYNOM1:func 6,a,p^q)       instead of          a*(p^q)
> >
> >  Sum URN(FVSUM_1:func 9,a,p)      instead of          Sum(a*p)
> 
> I think that this kind of naming _only_ should be available
> for redefinitions.  Else it might get to popular :-) and spoil
> the readability of the MML.

One solution is to allow such names only for introducing some normal 
synonyms for them. Even better if such "local synonyms" had to be 
part of the environment declarations. There could be a rule, that if the 
synonym becomes popular in more than one article, it will be moved right 
after the original definition.
But it also seems to me that rather than "POLYNOM1:func 6", some more 
explanatory absolute names would be better, especially if MML wants to 
become a semantic base for other projects.

Josef