Email Gateway (Aug 18 2022 at 17:08): Email Gateway (Aug 18 2022 at 17:08):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 17:08):From: Tjark Weber <webertj@in.tum.de>
Viorel,
Have you tried "apply (unfold class.some_algebra_def)"?
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 17:08):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Tjark,
This has worked well. Thank you.
Viorel
Last updated: Nov 21 2024 at 12:39 UTC