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

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr Rudnicki,

>I may be biased, I do not like "then" at all and am quite
>happy with using labels.

But even if my wish were implemented, you could just still do
it the other way, couldn't you?  I mean that's not a reason
_against_ it?  Or wouldn't you even like to read a proof by
someone else that would use then-after-consider.

I thought of one more reason for this.  Because then "let
... such that ..." would be more equivalent to "let ...;
assume ..." and "assume that ... and ..." would be more
equivalent to "assume ...; assume ...".  Now I write "let
...; assume ..." instead of "let ... such that ..." in order
to be able to use "then".

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

And "thus now" for "hereby" no doubt :-)  Our tastes clearly
differ.  That in its turn would not be interesting to me.

Freek