Re: [mizar] How to search for a lemma?

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

On Mon, 17 Mar 2003, Andrzej Trybulec wrote:

> > Are you planning/working on st. like that?
> 
> I would like to discuss it, at least. I am a bit uneasy about it (even if it is
> definetely in Mizar style). 

Obviously it could be misused - as any automation in Mizar - to hide from 
the proof presentation an important part. But it is rather general 
problem. 

> but at least theorems about real numbers can be used for elements of 
> <REAL,+> and vice versa, but then most of them will be proved for reals.

Actually I just realized that the requirement that both sides of the 
equation must match would prevent current equalizer from that in cases 
like: 
a*(b*c) = (a*b)*c by AXIOMS:13;

because the terms in AXIOMS:13 are universally quantified. So the 
matching would have to be tried also after equalizer.

> The identification is maybe wrong name. We already overuse it (identification of
> identifiers, identification of symbols).

"definition" would correspond to the terminology for clusters, but as 
Armstrong noted, it is quite strange. How about some common pragma for
such "automatizing" items? 

Josef