# [isabelle] unfolding classes

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] unfolding classes
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Mon, 28 Feb 2011 17:15:52 +0200
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.13) Gecko/20101207 Lightning/1.0b2 Thunderbird/3.1.7

Hello,
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.
``If I try apply unfold_locales the goal does not change. If I start with
``proof I get
`class.some_algebra (1:: bool) (op * :: bool => bool => bool) ==> False
which still does not unfold class.some_algebra.
I am still using Isabelle 2009-2.
Best regards,
Viorel

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