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


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?

Manuel Eberl

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