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.

Larry


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.