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

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