Re: [isabelle] Modify theorem with equality assumption


Am Donnerstag, den 02.04.2015, 17:46 +0200 schrieb Manuel Eberl:
> 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?

foo[unfolded eq_thm] or foo[folded eq_thm] do it in Isabelle/Isar; not
sure about Isabelle/ML.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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