Re: [mizar] Strong Mizar wish: linking to consider

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

> It is not clear to me what are the big savings.  With Freek's proposal
> we save one label after conditions provided that we link only
> to the last proposition and we never refer to this proposition later.
>

I must ask somebody to do statistics: how often in MML occurs situation when we
spare something (a label, a reference) if linking after the Choice Statement is
allowed.

>
> If any enhancements are planned to "then", then I am willing to bribe
> someone to allow "then thus".

What about "thus then". Please observe that the grammar allows it:

Conclusion   =   (   thus   |   hence   )   Statement   .
Statement   =   [   then   ]   Linkable-Statement   |   Diffuse-Statement   .

Unfortunately it allows even "hence then". Once we have contraction "thus now"
to "hereby", the contraction "thus then" to "hence" should be allowed, too.

BTW. Should the decomposition (to two tokens) be done in TOKENIZER or in PARSER?

Andrzej