Re: [isabelle] unfolding classes



Tjark,

This has worked well. Thank you.

Viorel

On 2/28/2011 5:26 PM, Tjark Weber wrote:
Viorel,

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
class.some_algebra.
Have you tried "apply (unfold class.some_algebra_def)"?

Kind regards,
Tjark










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