Hi Freek, On Fri, 3 Feb 2006, Freek Wiedijk wrote:
But this will generally happen often, references will be lemmas proved/assumed in parent blocks, are you sure you do not want them?Ah, I was not clear enough, I see. Yes, _those_ I generally certainly want! I just meant that I don't want references to labels at "article top level" so outside _any_ block.
But there is no difference between them and the lemmas proved at lower blocks in Mizar, look e.g. at the beginning of CARD_1: http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html.937/card_1.html - it's a non-theorem top-level lemma, used in other proofs. I am not happy with this, but such lemmas may even contain local constants if such constants are introduced at the top-level block (e.g. by (re)considering).
Best, Josef