Email Gateway (Nov 07 2020 at 18:10): 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
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: Jul 15 2022 at 23:21 UTC