Re: [isabelle] substituting in hypotheses

In the developer's version of Isabelle (and in the next release) you can do this:

apply (subst (asm) L1)

The new version of subst also lets you specify which instance of the LHS to substitute for, and many other things. All thanks to Lucas Dixon.


On 24 Aug 2005, at 03:44, John Matthews wrote:

When proving "silly" I'd like to use lemma L1 to substitute "x+1+0" for "x+1" in the second hypotheses. Note that

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