[isabelle] Referring to "this" in "from" and "using"
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Referring to "this" in "from" and "using"
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Fri, 15 Jun 2012 16:46:39 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1
I noticed that the following works:
from B[OF this] have C
Whereas this does not:
have C using B[OF this]
The error message is "Unknown fact 'this'".
Is this intended behaviour, and if yes, why?
This archive was generated by a fusion of
Pipermail (Mailman edition) and