[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:184.108.40.206) Gecko/20101207 Lightning/1.0b2 Thunderbird/3.1.7
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and