[isabelle] scope of facts arising from `subgoal`



Hi,

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?

cheers,
peter





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