Re: [isabelle] Modify theorem with equality assumption

On Thu, 2 Apr 2015, Manuel Eberl wrote:

I now want to derive modified theorems from them by adding an assumption
"p = ?q" (for a schematic variable ?q) and replace all occurrences of p
in the assumptions and the conclusion with ?q. Ideally in ML.

Another variation: fix q locally, then work with non-schematic material inside the extended context (which is usually easier and more robust), then export the result into the original context to make q schematic.


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