*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Beginner's struggles*From*: Ian Lynagh <igloo at earth.li>*Date*: Mon, 16 Aug 2010 16:51:15 +0100*In-reply-to*: <20100815143729.GA12552@matrix.chaos.earth.li>*References*: <20100814004117.GA19807@matrix.chaos.earth.li> <alpine.LNX.1.10.1008141659380.5958@atbroy100.informatik.tu-muenchen.de> <20100815143729.GA12552@matrix.chaos.earth.li>*User-agent*: Mutt/1.5.18 (2008-05-17)

On Sun, Aug 15, 2010 at 03:37:30PM +0100, Ian Lynagh wrote: > > the "proof state" is the same before and after the "fix a" line > Am I missing something? Perhaps the question I should really have asked is: Given a proof state of goal (1 subgoal): 1. !!x. P (f x) why does "fix a" not give a proof state of: goal (1 subgoal): 1. P (f a) ? Thanks Ian

**References**:**[isabelle] Beginner's struggles***From:*Ian Lynagh

**Re: [isabelle] Beginner's struggles***From:*Makarius

**Re: [isabelle] Beginner's struggles***From:*Ian Lynagh

- Previous by Date: [isabelle] PhD position in Computational Logic at the University of Innsbruck
- Next by Date: [isabelle] stuck on proof
- Previous by Thread: Re: [isabelle] Beginner's struggles
- Next by Thread: Re: [isabelle] Beginner's struggles
- Cl-isabelle-users August 2010 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