[isabelle] unfolding classes



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.