Re: [isabelle] Beginner's struggles



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






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