[isabelle] Unfolding constant defintiions
- To: <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Unfolding constant defintiions
- From: "Janney, Mark-P26816" <Mark.Janney at gdc4s.com>
- Date: Thu, 22 Feb 2007 15:20:40 -0700
- Thread-index: AcdWz68yRBhG2WCjRumuDyimxx4eHQ==
- Thread-topic: 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