Re: [mizar] Now I know why I cannot quote a theorem as the sawdust remains

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Tue, Dec 02, 2003 at 11:50:21AM +0100, Adam Grabowski wrote:
> On Sat, 29 Nov 2003, Piotr Rudnicki wrote:
> 
> > I need both notations from FVSUM1 and from POLYNOM1.  What am I supposed
> > to do?
>   Maybe slightly off-topic, but aren't the two definenses equivalent?
> At least I have just proven their compatibility. Maybe the best solution
> is to change the definition from POLYNOM1 into the redefinition and I
> think it should be done.
>   URN problem remains unsolved, however.

Certainly this would solve my problem at hand.

I can wait until the POLYNOM1 is revised.  On the other hand if you
look at the authors fo POLYNOM1, one can wonder why that redefinition
has not been done in the original article.

I agree that the URN issue can be postponed but it will not go away.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr