[isabelle] scope of facts arising from `subgoal`
I’m a bit surprised that the cartouches don’t seem to know about facts arising from the `subgoal` construct. Here’s an example:
lemma "mono id"
apply (rule monoI)
subgoal for x y
using arg_cong[OF ‹x ≤ y›]
Using a recent (unmentionable on this mailing list) version of Isabelle, I get:
Failed to retrieve literal fact⌂:
x ≤ y
The motivation for this is that a tool I’m using wants to have such facts passed in explicitly, i.e. it wants
apply (method ‹x ≤ y›)
I think this is the right UI for it; like `subst` it is a precise and low-level method, and so shouldn’t pick up arbitrary hypotheses from the goal or other contexts.
Can we change the behavior of `subgoal` or log this behavior somewhere?
This archive was generated by a fusion of
Pipermail (Mailman edition) and