Re: [mizar] Hindrances

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

On Thu, 7 Nov 2002, Andrzej Trybulec wrote:

> What really hinders the work with MML, it is using different
> formulations of the same fact in different theorems. The typical
> example:
>  sometimes it is  'i < j' sometimes 'i+1 <= j'
> and one has to use NAT_1:38 to move from one to the other.

In "ideal" system, I would want to have both, and I would want the system 
to understand that they are equivalent without the reference. I believe
that implementation is quite possible. The hard part is to say which 
equivalences should be obvious. Making it user-dependent is a bit dangerous.

Josef