Email Gateway (Jul 08 2021 at 13:35): Email Gateway (Jul 08 2021 at 13:35):From: Yann Leray <yann.leray@inria.fr>
Hi,
I'd like to use the proof term syntax, as defined in implementation
§2.5, to prove theorems (more precisely, I'd like to translate some
proof terms to asyntax understood by Isabelle).
However, there is no mention in this documentation of a command to use
the proof term to prove theorems directly inside Isabelle.
As far as I understand, Proof_Checker.thm_of_proof can return a value
of the type thm, which is what I would want, but I don't know how to
export it as a theorem in Isabelle.
How should I do to export this returned value (if I understood well) ?
Thanks for your time
Yann Leray
Last updated: Apr 19 2024 at 20:15 UTC