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