[isabelle] Unfolding constant defintiions



Here's a newbie question:

I frequently find that I have some constant, zot, having a fairly
complex definition, zot_def.

Then in some proof I want to say things like
    have "zot x y z = ZOT(x,yz)" 
where ZOT(x,yz) the unfolded definition of zot with the actual
parameters x, y, z, substituted in for the formal parameters.

So far I have done the unfolding manually via cut-n-paste, which is
tedious and error-prone.

Is there any way to get Isabelle to perform the unfolding for me?

Thanks - Mark Janney









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