Yann Leray (Jul 09 2021 at 19:12): Yann Leray (Jul 09 2021 at 19:12):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 a syntax 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, ML function 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) ?
TL; DR: How do I use a ML function returning a value of type thm to prove a theorem in the outer syntax ?
Lukas Stevens (Jul 09 2021 at 19:24):See page 18 of the ML cookbook. In particular, you are looking for the function Local_Theory.note.
Last updated: Dec 21 2024 at 16:20 UTC