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,
-john






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