[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
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