Re: Linking facts emerging from consider/given?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Thu, Apr 05, 2001 at 08:32:47PM +0200, Markus Wenzel wrote:
> 
> According to some Mizar documentation which I do not remember now, local
> results emerging from "consider" or "given" may not be linked (via "then"
> or "hence").  Indeed this is what Mizar has to say about that situation:
> 
>   consider x such that x = y; then y = x;
>   :: consider/given may not be used with linking!?
>   ::>  *164                             *164
> 
> This restriction looks quite arbitrary for me.  Is there any good reason
> why this is so?  The key feature of consider/given versus other statements
> that produce facts appears to be that multiple results may emerge
> simultaneaously.  

Similarly for:

	assume that ...
	let ... such that ...

If multiple conditions are used then the linkage would be
to what?  Their conjunction?  I do not like it.

> So I would suspect that this might be *some* reason for
> this slightly odd end.  

The above is a good enough reason for me.

If I may: I hate linkage for I never can decide whether 'then' belongs at
the end of a line or at the beginning.  My favourite solution is to use
a standard label say "_previous" and instead of 

	... ; then ... by ...

I would like to have

	... ; ... by _previous, ...


-- 
Piotr Rudnicki               CompSci, Univerity of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr