Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Definitional axioms in Isabelle/ML?


view this post on Zulip Email Gateway (Nov 07 2020 at 18:10):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I would like to understand if it is possible to recover the original
definitional axioms (i.e. the ones of the form c≡t) in the form of a
theorem for any given constant by the end-users of Isabelle/ML. If so, how
can this be achieved? If not, what are the reasons for not allowing this?

Kind Regards,
Mikhail Chekhov

view this post on Zulip Email Gateway (Nov 07 2020 at 19:12):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

Please accept my apologies for a premature question. I found a way to do
it: it can be done using the function Thm.axiom, if one knows the name of
the definitional axiom (which is also sufficiently easy to obtain).

Kind Regards,
Mikhail Chekhov


Last updated: Dec 05 2021 at 22:18 UTC