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

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

Hi, 

On Mon, 17 Mar 2003, Andrzej Trybulec wrote:

> For real numbers the following structures already defined in Mizar may
> be used candidates as well:
> ....

This seems to me rather a trouble with structures and identification 
mechanisms generally. I would most probably want a real number to be 
Element of all the structures you show (if present in environment).
A hack in this direction could be st. like:

definition let S be set;
  redefine mode Element of S -> Element of 1-sorted(# S #);
  coherence by STRUCT_0:def 2;
end; 

But it is not enough for current Mizar. I really think we could save 
ourselves a lot of problems like this, if we re-thought the structure 
mechanisms and had as much automatization as e.g. in the cluster 
mechanisms, which work comparatively well.

Regards,
Josef