*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 13:45:38 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5523AB30.6000505@in.tum.de>*References*: <551D646E.9060508@in.tum.de> <5AD61EC4-4357-4542-A826-081AB4BE3623@inria.fr> <551DB1BE.9050308@in.tum.de> <A9D5660E-91C3-413E-925D-9AECE3D68775@inria.fr> <551E6982.6090606@in.tum.de> <alpine.LNX.2.00.1504071148500.53483@lxbroy10.informatik.tu-muenchen.de> <5523AB30.6000505@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 7 Apr 2015, Manuel Eberl wrote:

"The" repository version is undefined, until "hg id" is used.e83ecf0a0ee1. I usually make a point of pulling the latest version regularly to keep my developments up-to-date.

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.Is that not what I did in the end? (q being p')

Makarius

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

**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

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

**Re: [isabelle] Modify theorem with equality assumption***From:*Jasmin Blanchette

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

**Re: [isabelle] Modify theorem with equality assumption***From:*Makarius

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

- Previous by Date: Re: [isabelle] Modify theorem with equality assumption
- Next by Date: Re: [isabelle] \forall versus \And -- also \exists versus \Or
- Previous by Thread: Re: [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