Re: [isabelle] substituting in hypotheses

Hi Larry and Jeremy (and Lucas),

The "subst (asm)" method worked well in my current Isabelle theory. Jeremy, your extensive conversions library also looks very useful for fine-grained control over rewriting, as does your file for manipulating Isar contexts within ML.

Thanks for the tips,

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