*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Modify theorem with equality assumption*From*: Makarius <makarius at sketis.net>*Date*: Tue, 7 Apr 2015 11:59:11 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <551D646E.9060508@in.tum.de>*References*: <551D646E.9060508@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.

Makarius

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

- Previous by Date: Re: [isabelle] Modify theorem with equality assumption
- Next by Date: Re: [isabelle] Modify theorem with equality assumption
- Previous by Thread: Re: [isabelle] Modify theorem with equality assumption
- Next by Thread: [isabelle] An induction rule
- 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