Re: [isabelle] unfolding classes



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.