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

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr,

>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.

Freek