*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 02 Apr 2015 18:00:13 +0200*In-reply-to*: <551D646E.9060508@in.tum.de>*References*: <551D646E.9060508@in.tum.de>

Hi, 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. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Modify theorem with equality assumption***From:*Joachim Breitner

**References**:**[isabelle] Modify theorem with equality assumption***From:*Manuel Eberl

- Previous by Date: [isabelle] Modify theorem with equality assumption
- Next by Date: Re: [isabelle] Modify theorem with equality assumption
- Previous by Thread: [isabelle] Modify theorem with equality assumption
- Next by Thread: Re: [isabelle] Modify theorem with equality assumption
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list