Re: [isabelle] unfolding classes
This has worked well. Thank you.
On 2/28/2011 5:26 PM, Tjark Weber wrote:
On Mon, 2011-02-28 at 17:15 +0200, Viorel Preoteasa wrote:
I want to a lemma like:
lemma "¬ class.some_algebra (1:: bool) (op * :: bool => bool => bool)"
I can write this lemma, however I don't know how to unfold
Have you tried "apply (unfold class.some_algebra_def)"?
This archive was generated by a fusion of
Pipermail (Mailman edition) and