[isabelle] Modify theorem with equality assumption


I have a number of theorems that contain some constant p both in their
assumptions and in their conclusions.

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.

What is the easiest way to do that?



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