Re: [isabelle] Referring to "this" in "from" and "using"



Am 15/06/2012 16:46, schrieb Manuel Eberl:
> Hallo,
> 
> I noticed that the following works:
> note A
> from B[OF this] have C
> 
> Whereas this does not:
> note A
> have C using B[OF this]
> 
> The error message is "Unknown fact 'this'".
> 
> Is this intended behaviour, and if yes, why?

I believe this is intended: after "have P", "this" should refer to P, but since
P has not been proved at "using", "this" is not defined just yet.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.