# [isabelle] Modify theorem with equality assumption

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Modify theorem with equality assumption
*From*: Manuel Eberl <eberlm at in.tum.de>
*Date*: Thu, 02 Apr 2015 17:46:54 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

Hallo,
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?
Cheers,
Manuel

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